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

changeset 1426:800218d431dc

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 Sat, 01 Jul 2023 16:03:54 +0900
parents a0e8df81a466
children 2134c62fdc30
files src/cardinal.agda
diffstat 1 files changed, 8 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Sat Jul 01 16:03:42 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 01 16:03:54 2023 +0900
@@ -429,6 +429,14 @@
            be77 : odef (* (& a-UC)) (fba x (proj1 (subst (λ k → odef k x) *iso be76)))
            be77 = subst (λ k → odef k (fba x (proj1 (subst (λ k → odef k x) *iso be76)) )) (sym *iso) 
                ⟪ a∋fba x (proj1 (subst (λ k → odef k x) *iso be76)) , ? ⟫
+           be78 : fba x (proj1 (subst (λ k → odef k x) *iso be76)) p
+              (sym *iso) ⟪ proj1 (subst₂ (λ A → OD.def (od A)) *iso refl (subst (λ k → OD.def (od k) (fba x
+                    (proj1 (subst (λ k₁ → OD.def (od k₁) x) *iso (subst (λ k₁ → OD.def (od k₁) x) (sym *iso)
+                       ⟪ bx , subst (λ k₁ → OD.def (od k₁) x → ⊥) (sym *iso) x₁ ⟫))))) (sym *iso)
+                ⟪ a∋fba x (proj1 (subst (λ k → OD.def (od k) x) *iso (subst (λ k → OD.def (od k) x) (sym *iso)
+                   ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫))) , (λ cn →
+                   cardinal.be25 O fab b∋fab fab-inject fba a∋fba fba-inject x (subst (λ k → OD.def (od k) x) (sym *iso)
+                    ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫) cn | cn) ⟫)) , c2 ⟫))
 
 
       be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) →  h⁻¹ (be70 x ax cc0) (cc11 ax cc0) ≡ x