Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff zf.agda @ 30:3b0fdb95618e
problem on Ordinal ( OSuc ℵ )
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 21 May 2019 00:30:01 +0900 |
| parents | fce60b99dc55 |
| children | c9ad0d97ce41 |
line wrap: on
line diff
--- a/zf.agda Mon May 20 18:18:43 2019 +0900 +++ b/zf.agda Tue May 21 00:30:01 2019 +0900 @@ -80,8 +80,8 @@ -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w ) extentionality : ( A B z : ZFSet ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) ) - minimul : ZFSet → ZFSet - regularity : ∀( x : ZFSet ) → ¬ (x ≈ ∅) → ( minimul x ∈ x ∧ ( minimul x ∩ x ≈ ∅ ) ) + minimul : ZFSet → ( ZFSet ∧ ZFSet ) + regularity : ∀( x : ZFSet ) → ¬ (x ≈ ∅) → ( proj1 ( minimul x ) ∈ x ∧ ( proj1 ( minimul x ) ∩ x ≈ ∅ ) ) -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) ) infinity∅ : ∅ ∈ infinite infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ Select X ( λ y → x ≈ y )) ∈ infinite