Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison HOD.agda @ 129:2a5519dcc167

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ord power set
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 02 Jul 2019 09:28:26 +0900
parents 69a845b82854
children 3849614bef18
comparison
equal deleted inserted replaced
128:69a845b82854 129:2a5519dcc167
58 58
59 postulate 59 postulate
60 -- HOD can be iso to a subset of Ordinal ( by means of Godel Set ) 60 -- HOD can be iso to a subset of Ordinal ( by means of Godel Set )
61 od→ord : {n : Level} → HOD {n} → Ordinal {n} 61 od→ord : {n : Level} → HOD {n} → Ordinal {n}
62 ord→od : {n : Level} → Ordinal {n} → HOD {n} 62 ord→od : {n : Level} → Ordinal {n} → HOD {n}
63 c<→o< : {n : Level} {x y : HOD {n} } → def y ( od→ord x ) → od→ord x o< od→ord y
63 oiso : {n : Level} {x : HOD {n}} → ord→od ( od→ord x ) ≡ x 64 oiso : {n : Level} {x : HOD {n}} → ord→od ( od→ord x ) ≡ x
64 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x 65 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
65 c<→o< : {n : Level} {x y : HOD {n} } → def y ( od→ord x ) → od→ord x o< od→ord y
66 ord-Ord :{n : Level} {x : Ordinal {n}} → x ≡ od→ord (Ord x) 66 ord-Ord :{n : Level} {x : Ordinal {n}} → x ≡ od→ord (Ord x)
67 ==→o≡ : {n : Level} → { x y : HOD {suc n} } → (x == y) → x ≡ y 67 ==→o≡ : {n : Level} → { x y : HOD {suc n} } → (x == y) → x ≡ y
68 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set 68 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
69 -- o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → def (ord→od y) x 69 -- o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → def (ord→od y) x
70 -- supermum as Replacement Axiom 70 -- supermum as Replacement Axiom
240 lemma : {z : Ordinal} → def A z ∧ def x z → {y : Ordinal} → y o< z → def A y ∧ def x y 240 lemma : {z : Ordinal} → def A z ∧ def x z → {y : Ordinal} → y o< z → def A y ∧ def x y
241 lemma {z} d {y} y<z = record { proj1 = otrans A (proj1 d) y<z ; proj2 = otrans x (proj2 d) y<z } 241 lemma {z} d {y} y<z = record { proj1 = otrans A (proj1 d) y<z ; proj2 = otrans x (proj2 d) y<z }
242 242
243 Def : {n : Level} → (A : HOD {suc n}) → HOD {suc n} 243 Def : {n : Level} → (A : HOD {suc n}) → HOD {suc n}
244 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) 244 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
245
246 OrdSubset : {n : Level} → (A x : Ordinal {suc n} ) → ZFSubset (Ord A) (Ord x) ≡ Ord ( minα A x )
247 OrdSubset {n} A x = ===-≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
248 lemma1 : {y : Ordinal} → def (ZFSubset (Ord A) (Ord x)) y → def (Ord (minα A x)) y
249 lemma1 {y} s with trio< A x
250 lemma1 {y} s | tri< a ¬b ¬c = proj1 s
251 lemma1 {y} s | tri≈ ¬a refl ¬c = proj1 s
252 lemma1 {y} s | tri> ¬a ¬b c = proj2 s
253 lemma2 : {y : Ordinal} → def (Ord (minα A x)) y → def (ZFSubset (Ord A) (Ord x)) y
254 lemma2 {y} lt with trio< A x
255 lemma2 {y} lt | tri< a ¬b ¬c = record { proj1 = lt ; proj2 = ordtrans lt a }
256 lemma2 {y} lt | tri≈ ¬a refl ¬c = record { proj1 = lt ; proj2 = lt }
257 lemma2 {y} lt | tri> ¬a ¬b c = record { proj1 = ordtrans lt c ; proj2 = lt }
245 258
246 -- Constructible Set on α 259 -- Constructible Set on α
247 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x } 260 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x }
248 -- L (Φ 0) = Φ 261 -- L (Φ 0) = Φ
249 -- L (OSuc lv n) = { Def ( L n ) } 262 -- L (OSuc lv n) = { Def ( L n ) }
294 _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n} 307 _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n}
295 x , y = Ord (omax (od→ord x) (od→ord y)) 308 x , y = Ord (omax (od→ord x) (od→ord y))
296 Union : HOD {suc n} → HOD {suc n} 309 Union : HOD {suc n} → HOD {suc n}
297 Union U = cseq U 310 Union U = cseq U
298 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) 311 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x )
299 Power : HOD {suc n} → HOD {suc n}
300 Power A = Def A
301 ZFSet = HOD {suc n} 312 ZFSet = HOD {suc n}
302 _∈_ : ( A B : ZFSet ) → Set (suc n) 313 _∈_ : ( A B : ZFSet ) → Set (suc n)
303 A ∈ B = B ∋ A 314 A ∈ B = B ∋ A
304 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) 315 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n)
305 _⊆_ A B {x} = A ∋ x → B ∋ x 316 _⊆_ A B {x} = A ∋ x → B ∋ x
306 _∩_ : ( A B : ZFSet ) → ZFSet 317 _∩_ : ( A B : ZFSet ) → ZFSet
307 A ∩ B = Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) ) 318 A ∩ B = Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) )
319 Power : HOD {suc n} → HOD {suc n}
320 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
308 -- _∪_ : ( A B : ZFSet ) → ZFSet 321 -- _∪_ : ( A B : ZFSet ) → ZFSet
309 -- A ∪ B = Select (A , B) ( λ x → (A ∋ x) ∨ ( B ∋ x ) ) 322 -- A ∪ B = Select (A , B) ( λ x → (A ∋ x) ∨ ( B ∋ x ) )
310 ｛_｝ : ZFSet → ZFSet 323 ｛_｝ : ZFSet → ZFSet
311 ｛ x ｝ = ( x , x ) 324 ｛ x ｝ = ( x , x )
312 325
319 ; pair = pair 332 ; pair = pair
320 ; union-u = λ X z UX∋z → union-u {X} {z} UX∋z 333 ; union-u = λ X z UX∋z → union-u {X} {z} UX∋z
321 ; union→ = union→ 334 ; union→ = union→
322 ; union← = union← 335 ; union← = union←
323 ; empty = empty 336 ; empty = empty
324 ; power→ = power→ 337 ; power→ = power→
325 ; power← = power← 338 ; power← = power←
326 ; extensionality = extensionality 339 ; extensionality = extensionality
327 ; minimul = minimul 340 ; minimul = minimul
328 ; regularity = regularity 341 ; regularity = regularity
329 ; infinity∅ = infinity∅ 342 ; infinity∅ = infinity∅
330 ; infinity = λ _ → infinity 343 ; infinity = λ _ → infinity
331 ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y} 344 ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
332 ; replacement = replacement 345 ; replacement = replacement
333 } where 346 } where
347
334 pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 348 pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
335 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B) 349 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
336 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B) 350 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
351
337 empty : (x : HOD {suc n} ) → ¬ (od∅ ∋ x) 352 empty : (x : HOD {suc n} ) → ¬ (od∅ ∋ x)
338 empty x (case1 ()) 353 empty x (case1 ())
339 empty x (case2 ()) 354 empty x (case2 ())
355
340 --- 356 ---
341 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A 357 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A
342 --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A 358 --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A
343 -- 359 --
344 -- if Power A ∋ t, from a propertiy of minimum sup there is osuc ZFSubset A ∋ t 360 -- if Power A ∋ t, from a propertiy of minimum sup there is osuc ZFSubset A ∋ t
345 -- then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x 361 -- then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x
346 -- In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity 362 -- In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity
347 -- 363 --
348 POrd : {A t : HOD} → Power A ∋ t → Power A ∋ Ord (od→ord t) 364 POrd : {a : Ordinal } {t : HOD} → Def (Ord a) ∋ t → Def (Ord a) ∋ Ord (od→ord t)
349 POrd {A} {t} P∋t = o<→c< P∋t 365 POrd {a} {t} P∋t = o<→c< P∋t
350 power→ : (A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x 366 ord-power→ : (a : Ordinal ) ( t : HOD) → Def (Ord a) ∋ t → {x : HOD} → t ∋ x → Ord a ∋ x
351 power→ A t P∋t {x} t∋x with osuc-≡< (sup-lb (POrd P∋t)) 367 ord-power→ a t P∋t {x} t∋x with osuc-≡< (sup-lb (POrd P∋t))
352 ... | case1 eq = proj1 (def-subst (Ltx t∋x) (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl ) where 368 ... | case1 eq = proj1 (def-subst (Ltx t∋x) (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl ) where
353 Ltx : {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x 369 Ltx : {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
354 Ltx {n} {x} {t} lt = c<→o< lt 370 Ltx {n} {x} {t} lt = c<→o< lt
355 ... | case2 lt = otrans A (proj1 (lemma1 lt) ) 371 ... | case2 lt = otrans (Ord a) (proj1 (lemma1 lt) )
356 (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) where 372 (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) where
373 sp = sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))
357 minsup : HOD 374 minsup : HOD
358 minsup = ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 375 minsup = ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))))
359 Ltx : {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x 376 Ltx : {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
360 Ltx {n} {x} {t} lt = c<→o< lt 377 Ltx {n} {x} {t} lt = c<→o< lt
361 lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t) 378 lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t)
362 lemma1 lt = {!!} 379 lemma1 lt with OrdSubset a ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))
380 ... | eq with subst ( λ k → ZFSubset (Ord a) k ≡ Ord (minα a sp)) Ord-ord eq
381 ... | eq1 = def-subst {suc n} {_} {_} {minsup} {od→ord (Ord (od→ord t))} (o<→c< lt) lemma2 (sym ord-Ord) where
382 lemma2 : Ord (od→ord (ZFSubset (Ord a) (ord→od sp))) ≡ minsup
383 lemma2 = let open ≡-Reasoning in begin
384 Ord (od→ord (ZFSubset (Ord a) (ord→od sp)))
385 ≡⟨ cong (λ k → Ord (od→ord k)) eq1 ⟩
386 Ord (od→ord (Ord (minα a sp)))
387 ≡⟨ cong (λ k → Ord (od→ord k)) Ord-ord ⟩
388 Ord (od→ord (ord→od (minα a sp)))
389 ≡⟨ cong (λ k → Ord k) diso ⟩
390 Ord (minα a sp)
391 ≡⟨ sym eq1 ⟩
392 minsup
393 ∎
394
363 -- 395 --
364 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t 396 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
365 -- Power A is a sup of ZFSubset A t, so Power A ∋ t 397 -- Power A is a sup of ZFSubset A t, so Power A ∋ t
366 -- 398 --
367 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t 399 ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
368 power← A t t→A = def-subst {suc n} {_} {_} {Power A} {od→ord t} 400 ord-power← a t t→A = def-subst {suc n} {_} {_} {Def (Ord a)} {od→ord t}
369 lemma refl (lemma1 lemma-eq )where 401 lemma refl (lemma1 lemma-eq )where
370 lemma-eq : ZFSubset A t == t 402 lemma-eq : ZFSubset (Ord a) t == t
371 eq→ lemma-eq {z} w = proj2 w 403 eq→ lemma-eq {z} w = proj2 w
372 eq← lemma-eq {z} w = record { proj2 = w ; 404 eq← lemma-eq {z} w = record { proj2 = w ;
373 proj1 = def-subst {suc n} {_} {_} {A} {z} 405 proj1 = def-subst {suc n} {_} {_} {(Ord a)} {z}
374 ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } 406 ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso }
375 lemma1 : {n : Level } { A t : HOD {suc n}} → (eq : ZFSubset A t == t) → od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t 407 lemma1 : {n : Level } {a : Ordinal {suc n}} { t : HOD {suc n}}
376 lemma1 {n} {A} {t} eq = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq )) 408 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
377 lemma : od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x))) 409 lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq ))
410 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
378 lemma = sup-o< 411 lemma = sup-o<
412
413 power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
414 power→ = {!!}
415 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
416 power← = {!!}
417
379 union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n} 418 union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}
380 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) ) 419 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
381 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 420 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
382 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z )) 421 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
383 union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx)) 422 union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx))
386 union→ X z u xx | tri> ¬a ¬b c = otrans X (proj1 xx) c 425 union→ X z u xx | tri> ¬a ¬b c = otrans X (proj1 xx) c
387 union← : (X z : HOD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z ) 426 union← : (X z : HOD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
388 union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where 427 union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
389 lemma : X ∋ union-u {X} {z} X∋z 428 lemma : X ∋ union-u {X} {z} X∋z
390 lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} X∋z refl ord-Ord 429 lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} X∋z refl ord-Ord
430
391 ψiso : {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y → ψ y 431 ψiso : {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y → ψ y
392 ψiso {ψ} t refl = t 432 ψiso {ψ} t refl = t
393 selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (((y₁ : HOD) → X ∋ y₁ → ψ y₁) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y) 433 selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (((y₁ : HOD) → X ∋ y₁ → ψ y₁) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y)
394 selection {X} {ψ} {y} = record { proj1 = λ s → record { 434 selection {X} {ψ} {y} = record { proj1 = λ s → record {
395 proj1 = λ y1 y1<X → proj1 s (ord→od y1) y1<X ; proj2 = subst (λ k → def X k ) (sym diso) (proj2 s) } 435 proj1 = λ y1 y1<X → proj1 s (ord→od y1) y1<X ; proj2 = subst (λ k → def X k ) (sym diso) (proj2 s) }
396 ; proj2 = λ s → record { proj1 = λ y1 dy1 → subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso ))) 436 ; proj2 = λ s → record { proj1 = λ y1 dy1 → subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso )))
397 ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where 437 ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where
438
398 replacement : {ψ : HOD → HOD} (X x : HOD) → Replace X ψ ∋ ψ x 439 replacement : {ψ : HOD → HOD} (X x : HOD) → Replace X ψ ∋ ψ x
399 replacement {ψ} X x = sup-c< ψ {x} 440 replacement {ψ} X x = sup-c< ψ {x}
441
400 ∅-iso : {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 442 ∅-iso : {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
401 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq 443 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
402 regularity : (x : HOD) (not : ¬ (x == od∅)) → 444 regularity : (x : HOD) (not : ¬ (x == od∅)) →
403 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 445 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
404 proj1 (regularity x not ) = x∋minimul x not 446 proj1 (regularity x not ) = x∋minimul x not
407 lemma1 {x₁} s = ⊥-elim ( minimul-1 x not (ord→od x₁) lemma3 ) where 449 lemma1 {x₁} s = ⊥-elim ( minimul-1 x not (ord→od x₁) lemma3 ) where
408 lemma3 : def (minimul x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁)) 450 lemma3 : def (minimul x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁))
409 lemma3 = proj1 s x₁ (proj2 s) 451 lemma3 = proj1 s x₁ (proj2 s)
410 lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ 452 lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁
411 lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {suc n} {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) )) 453 lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {suc n} {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) ))
454
412 extensionality : {A B : HOD {suc n}} → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A == B 455 extensionality : {A B : HOD {suc n}} → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
413 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d 456 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
414 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d 457 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
458
415 open import Relation.Binary.PropositionalEquality 459 open import Relation.Binary.PropositionalEquality
416 uxxx-ord : {x : HOD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) ) 460 uxxx-ord : {x : HOD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) )
417 uxxx-ord {x} {y} = subst (λ k → k ⇔ ( y o< osuc (od→ord x) )) (sym lemma) ( osuc2 y (od→ord x)) where 461 uxxx-ord {x} {y} = subst (λ k → k ⇔ ( y o< osuc (od→ord x) )) (sym lemma) ( osuc2 y (od→ord x)) where
418 lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x)) 462 lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x))
419 lemma {y} = let open ≡-Reasoning in begin 463 lemma {y} = let open ≡-Reasoning in begin