补丁（3）论文集合模型论部分篇。 (6-4)

设x是极限层, 要证y ∈ x蕴含 y ∈ x. 由引理1-3-11, 存在层z满足y ∈ z ∈ x. 对层x和层 z, 由层的ϵ线序, 分两种情况.

• 若 z ⊆ x, 由引理1-3-9有Ρ y ∈ Ρ z, 即得Ρ y ∈ x.

• 若x ∈ Ρ z, 即x ⊆ z, 由z ∈ x得到z ∈ z, 违反正则公理 ∎

　Lemma 极限层对幂集封闭 : 极限层 ⊑ 幂集封闭. Proof. intros x xL y yx. destruct (极限层对秩封闭 xL yx) as [z [zS [yz zx]]]. destruct xL as [xS _]. destruct (层线序 (幂层 zS) xS). - apply (幂_升秩 yz) in zS as pypz. auto. - exfalso. apply 幂集 in H. specialize (H z zx). now apply 无循环1 in H. Qed.

最后两种封闭性与主线无关, 我们略过它们的证明, 感兴趣的读者可以看Github仓库.

引理1-3-15 对集合做分离不改变其秩.

引理1-3-16 配对的秩高于原集合的秩.

Lemma 分离_等秩 x y P : x ∈ y → y ∈ₚ 层 → x ∩ₚ P ∈ y. Lemma 配对_升秩 a b x : a ∈ x → b ∈ x → {a, b} ∈ 幂 x.

事实1-3-17 极限层对配对封闭.

事实1-3-18 极限层对分离封闭.

Fact 极限层对配对封闭 : 极限层 ⊑ 配对封闭. Fact 极限层对分离封闭 : 极限层 ⊑ 分离封闭.

　宇宙

我们考虑封闭类内化为集合的情况.

定义1-3-19 我们说一个集合是宇宙, 当且仅当该集合的成员正好与某个封闭类的成员相吻合.

Notation "A =ₚ P" := (∀ x, x ∈ A ↔ x ∈ₚ P) (at level 70) : zf_scope. Definition 宇宙 u := ∃ P, 封闭类 P ∧ u =ₚ P.

本节将省略一些简单的证明代码, 都可在Github仓库查看.

引理1-3-20 (宇宙的封闭性) 宇宙对空集, 并集, 幂集, 替代封闭.

由宇宙的定义可以立即得证 ∎

Lemma 宇宙对空集封闭 : 宇宙 ⊑ 空集封闭. Lemma 宇宙对并集封闭 : 宇宙 ⊑ 并集封闭. Lemma 宇宙对幂集封闭 : 宇宙 ⊑ 幂集封闭. Lemma 宇宙对替代封闭 : 宇宙 ⊑ 替代封闭.

　引理1-3-21 (宇宙的封闭性) 宇宙对成员关系和子集关系封闭.

前者由封闭类的传递性得证. 后者由前者以及宇宙对幂集的封闭性得证 ∎

(* 对成员关系封闭 *) Lemma 宇宙传递 : 宇宙 ⊑ 传递. (* 对子集关系封闭 *) Lemma 宇宙膨胀 : 宇宙 ⊑ 膨胀.

　备注1-3-22 若封闭类集化为了宇宙, 那么该宇宙也可以重新类化为封闭类.

依定义 ∎

Remark 宇宙类化 u : 宇宙 u → 封闭类 (λ x, x ∈ u).

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。