Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 319:eef432aa8dfb
Union done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 03 Jul 2020 21:39:10 +0900 |
parents | 9e0c97ab3a4a |
children | 21203fe0342f |
comparison
equal
deleted
inserted
replaced
318:9e0c97ab3a4a | 319:eef432aa8dfb |
---|---|
277 ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))} | 277 ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))} |
278 Union : HOD → HOD | 278 Union : HOD → HOD |
279 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } | 279 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } |
280 ; odmax = osuc (od→ord U) ; <odmax = umax< } where | 280 ; odmax = osuc (od→ord U) ; <odmax = umax< } where |
281 umax< : {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U) | 281 umax< : {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U) |
282 umax< {y} not = {!!} | 282 umax< {y} not = lemma (FExists _ lemma1 not ) where |
283 lemma0 : {x : Ordinal} → def (od (ord→od x)) y → y o< x | |
284 lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso diso (c<→o< (subst (λ k → def (od (ord→od x)) k) (sym diso) x<y)) | |
285 lemma2 : {x : Ordinal} → def (od U) x → x o< od→ord U | |
286 lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (subst (λ k → def (od U) k) (sym diso) x<U)) | |
287 lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y) | |
288 lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) ) | |
289 lemma : ¬ ((od→ord U) o< y ) → y o< osuc (od→ord U) | |
290 lemma not with trio< y (od→ord U) | |
291 lemma not | tri< a ¬b ¬c = ordtrans a <-osuc | |
292 lemma not | tri≈ ¬a refl ¬c = <-osuc | |
293 lemma not | tri> ¬a ¬b c = ⊥-elim (not c) | |
283 _∈_ : ( A B : ZFSet ) → Set n | 294 _∈_ : ( A B : ZFSet ) → Set n |
284 A ∈ B = B ∋ A | 295 A ∈ B = B ∋ A |
285 | 296 |
286 OPwr : (A : HOD ) → HOD | 297 OPwr : (A : HOD ) → HOD |
287 OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) ) | 298 OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) ) |