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

changeset 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
files HOD.agda
diffstat 1 files changed, 6 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Mon Jul 08 12:13:19 2019 +0900
+++ b/HOD.agda	Mon Jul 08 12:34:08 2019 +0900
@@ -465,13 +465,15 @@
               lemma0 {x} t∋x = c<→o< (t→A t∋x)
               lemma3 : Def (Ord a) ∋ t
               lemma3 = ord-power← a t lemma0
+              lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
+              lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) (sym Ord-ord-≡) (∩-≡ t→A ) ))
               lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x))
-              lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {{!!}}
-              ... | lt = {!!}
+              lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
+              ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where
+                  lemma5 : od→ord (A ∩ Ord (od→ord t)) ≡ od→ord (A ∩ ord→od (od→ord t))
+                  lemma5 = cong (λ k → od→ord (A ∩ k )) Ord-ord
               lemma2 :  def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
               lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma4 }) ) where
-                  lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
-                  lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) (sym Ord-ord-≡) (∩-≡ t→A ) ))
 
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq