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

changeset 1236:59e927672b80

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tyconoff done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 09 Mar 2023 02:57:16 +0900
parents d2506e861dbf
children 54a63423f128
files src/Tychonoff.agda
diffstat 1 files changed, 38 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Thu Mar 09 02:31:41 2023 +0900
+++ b/src/Tychonoff.agda	Thu Mar 09 02:57:16 2023 +0900
@@ -681,7 +681,44 @@
 
          --  FQSet is in Projection ⁻¹  F
          FQSet⊆F : {x : Ordinal } → odef FQSet x →  odef (filter F) (& (ZFP P (* x) ))
-         FQSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = ?
+         FQSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F ty80 (subst (λ k → odef (filter F) k) (sym &iso) az) ty71 where
+             Rx : HOD
+             Rx = Replace' (* z) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy)))
+             PxRx∋z : * z ⊆ ZFP P Rx  
+             PxRx∋z {w} zw = subst (λ k → ZFProduct P Rx k ) ty70 ( ab-pair (zp1 b) record { z = w ; az = zw ; x=ψz = refl } ) where
+                 a = F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw) 
+                 b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw )
+                 ty73 : & (* (zπ2 a)) ≡ zπ2 b 
+                 ty73 = begin
+                     & (* (zπ2 a)) ≡⟨ &iso ⟩ 
+                     zπ2 a ≡⟨ cong zπ2 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b)) ⟩ 
+                     zπ2 b ∎  where open ≡-Reasoning
+                 ty70 : & < * (zπ1 b) , * (& (* (zπ2 a)))  > ≡ w
+                 ty70 with zp-iso (subst (λ k → odef (ZFP P Q) k) (sym &iso) (f⊆L F az _ zw )) 
+                 ... | eq = trans (cong₂ (λ j k → & < j , * k > ) refl ty73 ) (trans eq &iso ) 
+             ty71 : * z ⊆ ZFP P (* x) 
+             ty71 = subst (λ k → * z ⊆ ZFP P k ) ty72 PxRx∋z where
+                 ty72 : Rx ≡ * x 
+                 ty72 = begin
+                    Rx ≡⟨ sym *iso ⟩
+                    * (& Rx)  ≡⟨ cong (*) (sym x=ψz ) ⟩
+                    * x ∎ where open ≡-Reasoning
+             ty80 : Power (ZFP P Q) ∋ ZFP P (* x) 
+             ty80 y yx = isQ→PxQ ty81 (subst (λ k → odef k y ) *iso yx ) where
+                 ty81 : * x ⊆ Q 
+                 ty81 {w} xw with subst (λ k → odef k w) (trans (cong (*) x=ψz ) *iso ) xw
+                 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef Q k) (sym ty84) ty87 where
+                      a =  f⊆L F (subst (odef (filter F)) (sym &iso) az) (& (* z1)) 
+                                 (subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) az1))
+                      b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) (f⊆L F az _ az1 )
+                      ty87 : odef Q (zπ2 b)
+                      ty87 = zp2 b
+                      ty84 : w ≡ (zπ2 b)
+                      ty84 = begin
+                       w ≡⟨ trans x=ψz1 &iso ⟩
+                       zπ2 a ≡⟨ cong zπ2 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b )) ⟩
+                       zπ2 b  ∎ where open ≡-Reasoning
+
 
          uflq : UFLP TQ FQ UFQ
          uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ