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

comparison HOD.agda @ 143:21b9e78e9359

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
union remains
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Jul 2019 12:34:08 +0900
parents c30bc9f5bd0d
children 3ba37037faf4
comparison
equal deleted inserted replaced
142:c30bc9f5bd0d 143:21b9e78e9359
463 a = od→ord A 463 a = od→ord A
464 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x 464 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x
465 lemma0 {x} t∋x = c<→o< (t→A t∋x) 465 lemma0 {x} t∋x = c<→o< (t→A t∋x)
466 lemma3 : Def (Ord a) ∋ t 466 lemma3 : Def (Ord a) ∋ t
467 lemma3 = ord-power← a t lemma0 467 lemma3 = ord-power← a t lemma0
468 lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
469 lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) (sym Ord-ord-≡) (∩-≡ t→A ) ))
468 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x)) 470 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x))
469 lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {{!!}} 471 lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
470 ... | lt = {!!} 472 ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where
473 lemma5 : od→ord (A ∩ Ord (od→ord t)) ≡ od→ord (A ∩ ord→od (od→ord t))
474 lemma5 = cong (λ k → od→ord (A ∩ k )) Ord-ord
471 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) 475 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
472 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma4 }) ) where 476 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma4 }) ) where
473 lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
474 lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) (sym Ord-ord-≡) (∩-≡ t→A ) ))
475 477
476 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 478 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
477 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq 479 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
478 regularity : (x : OD) (not : ¬ (x == od∅)) → 480 regularity : (x : OD) (not : ¬ (x == od∅)) →
479 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 481 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)