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

comparison OD.agda @ 378:853ead1b56b8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 20 Jul 2020 17:22:16 +0900
parents d735beee689a
children d2cb5278e46d
comparison
equal deleted inserted replaced
377:d735beee689a 378:853ead1b56b8
338 rmax< lt = proj1 lt 338 rmax< lt = proj1 lt
339 339
340 d→∋ : ( a : HOD ) { x : Ordinal} → odef a x → a ∋ (ord→od x) 340 d→∋ : ( a : HOD ) { x : Ordinal} → odef a x → a ∋ (ord→od x)
341 d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt 341 d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt
342 342
343 --
344 -- If we have LEM, Replace' is equivalent to Replace
345 --
343 in-codomain' : (X : HOD ) → ((x : HOD) → X ∋ x → HOD) → OD 346 in-codomain' : (X : HOD ) → ((x : HOD) → X ∋ x → HOD) → OD
344 in-codomain' X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ((lt : odef X y) → x ≡ od→ord (ψ (ord→od y ) (d→∋ X lt) )))) } 347 in-codomain' X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ((lt : odef X y) → x ≡ od→ord (ψ (ord→od y ) (d→∋ X lt) )))) }
345
346 Replace' : (X : HOD) → ((x : HOD) → X ∋ x → HOD) → HOD 348 Replace' : (X : HOD) → ((x : HOD) → X ∋ x → HOD) → HOD
347 Replace' X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y) ))) ∧ def (in-codomain' X ψ) x } 349 Replace' X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y) ))) ∧ def (in-codomain' X ψ) x }
348 ; odmax = rmax ; <odmax = rmax< } where 350 ; odmax = rmax ; <odmax = rmax< } where
349 rmax : Ordinal 351 rmax : Ordinal
350 rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y))) 352 rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y)))
494 lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where 496 lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
495 lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y))) → (ord→od (od→ord x) =h= ψ (ord→od y)) 497 lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y))) → (ord→od (od→ord x) =h= ψ (ord→od y))
496 lemma3 {y} eq = subst (λ k → ord→od (od→ord x) =h= k ) oiso (o≡→== eq ) 498 lemma3 {y} eq = subst (λ k → ord→od (od→ord x) =h= k ) oiso (o≡→== eq )
497 lemma : ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)) ) 499 lemma : ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)) )
498 lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y)) oiso ( proj2 not2 )) 500 lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y)) oiso ( proj2 not2 ))
499
500 sup-c<' : {X x : HOD} → (ψ : (x : HOD) → X ∋ x → HOD) → X ∋ x → od→ord (ψ x ? ) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y) ? )))
501 sup-c<' {X} {x} ψ lt = subst (λ k → od→ord (ψ k ? ) o< _ ) oiso (sup-o< X lt )
502 replacement←' : (X x : HOD) {ψ : (x : HOD) → X ∋ x → HOD} → X ∋ x → Replace' X ψ ∋ ψ x ?
503 replacement←' X x {ψ} lt = record { proj1 = sup-c<' {X} {x} ψ lt ; proj2 = lemma } where
504 lemma : def (in-codomain' X ψ) (od→ord (ψ x ? ))
505 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = ? }))
506 replacement→' : (X x : HOD) → {ψ : (x : HOD) → X ∋ x → HOD} → (lt : Replace' X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y ? ))
507 replacement→' X x {ψ} lt = contra-position lemma (lemma2 (λ lt1 → ? )) where
508 lemma2 : ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y) ? )))
509 → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y) ? ))
510 lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
511 lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y) ? )) → (ord→od (od→ord x) =h= ψ (ord→od y) ? )
512 lemma3 {y} eq = subst (λ k → ord→od (od→ord x) =h= k ) oiso (o≡→== eq )
513 lemma : ( (y : HOD) → ¬ (x =h= ψ y ? )) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y) ? ) )
514 lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y) ? ) oiso ( proj2 not2 ))
515 501
516 --- 502 ---
517 --- Power Set 503 --- Power Set
518 --- 504 ---
519 --- First consider ordinals in HOD 505 --- First consider ordinals in HOD