### changeset 312:c1581ed5f38b

...
author Shinji KONO Thu, 02 Jul 2020 19:05:55 +0900 bf01e924e62e 8b5c8b685883 OD.agda 1 files changed, 15 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Tue Jun 30 11:08:22 2020 +0900
+++ b/OD.agda	Thu Jul 02 19:05:55 2020 +0900
@@ -88,6 +88,7 @@
od→ord : HOD  → Ordinal
ord→od : Ordinal  → HOD
c<→o<  :  {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y
+  ⊆→o≤  :   {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z)
oiso   :  {x : HOD }      → ord→od ( od→ord x ) ≡ x
diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
==→o≡ : { x y : HOD  } → (od x == od y) → x ≡ y
@@ -218,16 +219,11 @@
lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))

-
-OPwr :  (A :  HOD ) → HOD
-OPwr  A = Ord ( sup-o A ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )
-
record _⊆_ ( A B : HOD   ) : Set (suc n) where
field
incl : { x : HOD } → A ∋ x →  B ∋ x

open _⊆_
-
infixr  220 _⊆_

subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( x ⊆ A  )
@@ -236,6 +232,11 @@
; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt }
}

+power< : {A x : HOD  } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x
+power< {A} {x} x⊆A = ⊆→o≤  (λ {y} x∋y → subst (λ k →  def (od A) k) diso (lemma y x∋y ) ) where
+    lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y))
+    lemma y x∋y = incl x⊆A (subst (λ k → def (od x) k ) (sym diso) x∋y )
+
open import Data.Unit

ε-induction : { ψ : HOD  → Set (suc n)}
@@ -272,6 +273,10 @@
Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  } ; odmax = {!!} ; <odmax = {!!} }
_∈_ : ( A B : ZFSet  ) → Set n
A ∈ B = B ∋ A
+
+    OPwr :  (A :  HOD ) → HOD
+    OPwr  A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )
+
Power : HOD  → HOD
Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
-- ｛_｝ : ZFSet → ZFSet
@@ -393,9 +398,9 @@
lemma1 :  {a : Ordinal } { t : HOD }
→ (eq : ZFSubset (Ord a) t =h= t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
lemma1  {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
-              lemma2 : def (od (Ord a)) (od→ord t)
-              lemma2 = {!!}
-              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord a) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x)))
+              lemma2 : (od→ord t) o< (osuc (od→ord (Ord a)))
+              lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t)))
+              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x)))
lemma = sup-o< _ lemma2

--
@@ -433,8 +438,9 @@
≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
t
∎
+              --- (od→ord t) o< (sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x))))
lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
-              lemma7 = {!!}
+              lemma7 = ordtrans {!!} (sup-o< {!!} {!!})
lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  (λ x lt → od→ord (A ∩ (ord→od x))))
lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )```