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

设宇宙u. 左边到右边: 引理1-3-20已证宇宙对替代和空集封闭; 引理1-3-24已证宇宙是层; 只需证u ⊆ ⋃ u. 对任意x ∈ u, 由宇宙对秩封闭有ρ x ∈ u, 要证x ∈ ⋃ u. 我们证 x ∈ (ρ x) ∈ u.

• 对左边, 由幂集公理和ρ规范得证.

• 对右边, 由宇宙对幂集的封闭性得证.

　Theorem 宇宙等价于对替代封闭的非空极限层 u : 宇宙 u ↔ (替代封闭 u ∧ 非空 u ∧ 极限层 u). Proof. split; intros H. - repeat split. + now apply 宇宙对替代封闭. + exists ∅. now apply 宇宙对空集封闭. + now apply 宇宙是层. + intros x xu%宇宙对秩封闭; auto. apply 并集. exists (幂 (ρ x)). split. * apply 幂集, ρ规范. * now apply 宇宙对幂集封闭.

右边到左边: 只需证 (λ x, x ∈ u) 是封闭类, 这由层的传递性, 极限层的封闭性, 以及u对替代封闭的前提得证 ∎

- destruct H as [rc [ne [uS sub]]]. exists (λ x, x ∈ u). split. 2:easy. split. + intros x y xy yu. eapply 层传递; eauto. + now apply 非空层对空集封闭. + now apply 极限层对并集封闭. + now apply 极限层对幂集封闭. + apply rc. Qed.

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