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

comparison OPair.agda @ 420:53422a8ea836

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bijection
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 31 Jul 2020 17:42:25 +0900
parents 4af94768e372
children 44a484f17f26
comparison
equal deleted inserted replaced
419:4af94768e372 420:53422a8ea836
164 lemma1 : odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (od→ord (Replace A (λ a₁ → < a₁ , b >))) 164 lemma1 : odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (od→ord (Replace A (λ a₁ → < a₁ , b >)))
165 lemma1 = replacement← B b B∋b 165 lemma1 = replacement← B b B∋b
166 lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (od→ord < a , b >) 166 lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (od→ord < a , b >)
167 lemma2 = replacement← A a A∋a 167 lemma2 = replacement← A a A∋a
168 168
169 -- axiom of choice required
170 -- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (od→ord x)
171 -- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (od→ord k )) {!!} op-cons
172
173 x<nextA : {A x : HOD} → A ∋ x → od→ord x o< next (odmax A) 169 x<nextA : {A x : HOD} → A ∋ x → od→ord x o< next (odmax A)
174 x<nextA {A} {x} A∋x = ordtrans (c<→o< {x} {A} A∋x) ho< 170 x<nextA {A} {x} A∋x = ordtrans (c<→o< {x} {A} A∋x) ho<
175 171
176 A<Bnext : {A B x : HOD} → od→ord A o< od→ord B → A ∋ x → od→ord x o< next (odmax B) 172 A<Bnext : {A B x : HOD} → od→ord A o< od→ord B → A ∋ x → od→ord x o< next (odmax B)
177 A<Bnext {A} {B} {x} lt A∋x = osucprev (begin 173 A<Bnext {A} {B} {x} lt A∋x = osucprev (begin
199 lemma2 : od→ord (ord→od y) o< next (HOD.odmax A) 195 lemma2 : od→ord (ord→od y) o< next (HOD.odmax A)
200 lemma2 = ordtrans ( subst (λ k → od→ord (ord→od y) o< k ) (sym b) (c<→o< (d→∋ B ((proj2 (proj2 lt (pair x y))))))) ho< 196 lemma2 = ordtrans ( subst (λ k → od→ord (ord→od y) o< k ) (sym b) (c<→o< (d→∋ B ((proj2 (proj2 lt (pair x y))))))) ho<
201 lemma p lt | pair x y | tri> ¬a ¬b c = ordtrans (ω-opair (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y)))))) 197 lemma p lt | pair x y | tri> ¬a ¬b c = ordtrans (ω-opair (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y))))))
202 (A<Bnext c (subst (λ k → odef B k ) (sym diso) (proj2 (proj2 lt (pair x y)))))) (omax-x _ _ ) 198 (A<Bnext c (subst (λ k → odef B k ) (sym diso) (proj2 (proj2 lt (pair x y)))))) (omax-x _ _ )
203 199
204 ZFP⊗ : {A B : HOD} → ZFP A B ≡ A ⊗ B 200 ZFP⊆⊗ : {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
205 ZFP⊗ {A} {B} = ==→o≡ record { eq→ = lemma0 ; eq← = lemma1 } where 201 ZFP⊆⊗ {A} {B} {px} record { proj1 = (pair x y) ; proj2 = p2 } = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) )))
206 AxB : HOD 202
207 AxB = Replace B (λ b → Replace A (λ a → < a , b > )) 203 -- axiom of choice required
208 lemma0 : {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x 204 -- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (od→ord x)
209 lemma0 {px} record { proj1 = (pair x y) ; proj2 = p2 } = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) ))) 205 -- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (od→ord k )) {!!} op-cons
210 lemma1 : {x : Ordinal} → odef (A ⊗ B) x → odef (ZFP A B) x 206
211 lemma1 {x} lt with union← AxB (ord→od x) (d→∋ (A ⊗ B) lt)
212 ... | t = {!!}
213
214
215
216
217
218
219
220
221