Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftphtlem Structured version   Visualization version   GIF version
Theorem cvmliftphtlem 34297
Description: Lemma for cvmliftpht 34298. (Contributed by Mario Carneiro, 6-Jul-2015.)
Hypotheses
Ref Expression
cvmliftpht.b 𝐡 = βˆͺ 𝐢
cvmliftpht.m 𝑀 = (℩𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐺 ∧ (π‘“β€˜0) = 𝑃))
cvmliftpht.n 𝑁 = (℩𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐻 ∧ (π‘“β€˜0) = 𝑃))
cvmliftpht.f (πœ‘ β†’ 𝐹 ∈ (𝐢 CovMap 𝐽))
cvmliftpht.p (πœ‘ β†’ 𝑃 ∈ 𝐡)
cvmliftpht.e (πœ‘ β†’ (πΉβ€˜π‘ƒ) = (πΊβ€˜0))
cvmliftphtlem.g (πœ‘ β†’ 𝐺 ∈ (II Cn 𝐽))
cvmliftphtlem.h (πœ‘ β†’ 𝐻 ∈ (II Cn 𝐽))
cvmliftphtlem.k (πœ‘ β†’ 𝐾 ∈ (𝐺(PHtpyβ€˜π½)𝐻))
cvmliftphtlem.a (πœ‘ β†’ 𝐴 ∈ ((II Γ—t II) Cn 𝐢))
cvmliftphtlem.c (πœ‘ β†’ (𝐹 ∘ 𝐴) = 𝐾)
cvmliftphtlem.0 (πœ‘ β†’ (0𝐴0) = 𝑃)
Assertion
Ref Expression
cvmliftphtlem (πœ‘ β†’ 𝐴 ∈ (𝑀(PHtpyβ€˜πΆ)𝑁))
Distinct variable groups:   𝐴,𝑓   𝐡,𝑓   𝑓,𝐹   𝑓,𝐽   𝐢,𝑓   𝑓,𝐺   𝑓,𝐻   𝑃,𝑓
Allowed substitution hints:   πœ‘(𝑓)   𝐾(𝑓)   𝑀(𝑓)   𝑁(𝑓)
Proof of Theorem cvmliftphtlem
Dummy variables 𝑠 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvmliftpht.b . . . 4 𝐡 = βˆͺ 𝐢
2 cvmliftpht.m . . . 4 𝑀 = (℩𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐺 ∧ (π‘“β€˜0) = 𝑃))
3 cvmliftpht.f . . . 4 (πœ‘ β†’ 𝐹 ∈ (𝐢 CovMap 𝐽))
4 cvmliftphtlem.g . . . 4 (πœ‘ β†’ 𝐺 ∈ (II Cn 𝐽))
5 cvmliftpht.p . . . 4 (πœ‘ β†’ 𝑃 ∈ 𝐡)
6 cvmliftpht.e . . . 4 (πœ‘ β†’ (πΉβ€˜π‘ƒ) = (πΊβ€˜0))
71, 2, 3, 4, 5, 6cvmliftiota 34281 . . 3 (πœ‘ β†’ (𝑀 ∈ (II Cn 𝐢) ∧ (𝐹 ∘ 𝑀) = 𝐺 ∧ (π‘€β€˜0) = 𝑃))
87simp1d 1143 . 2 (πœ‘ β†’ 𝑀 ∈ (II Cn 𝐢))
9 cvmliftpht.n . . . 4 𝑁 = (℩𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐻 ∧ (π‘“β€˜0) = 𝑃))
10 cvmliftphtlem.h . . . 4 (πœ‘ β†’ 𝐻 ∈ (II Cn 𝐽))
11 cvmliftphtlem.k . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ (𝐺(PHtpyβ€˜π½)𝐻))
124, 10, 11phtpy01 24493 . . . . . 6 (πœ‘ β†’ ((πΊβ€˜0) = (π»β€˜0) ∧ (πΊβ€˜1) = (π»β€˜1)))
1312simpld 496 . . . . 5 (πœ‘ β†’ (πΊβ€˜0) = (π»β€˜0))
146, 13eqtrd 2773 . . . 4 (πœ‘ β†’ (πΉβ€˜π‘ƒ) = (π»β€˜0))
151, 9, 3, 10, 5, 14cvmliftiota 34281 . . 3 (πœ‘ β†’ (𝑁 ∈ (II Cn 𝐢) ∧ (𝐹 ∘ 𝑁) = 𝐻 ∧ (π‘β€˜0) = 𝑃))
1615simp1d 1143 . 2 (πœ‘ β†’ 𝑁 ∈ (II Cn 𝐢))
17 cvmliftphtlem.a . 2 (πœ‘ β†’ 𝐴 ∈ ((II Γ—t II) Cn 𝐢))
18 iitop 24388 . . . . . . . . . . . . . . . 16 II ∈ Top
19 iiuni 24389 . . . . . . . . . . . . . . . 16 (0[,]1) = βˆͺ II
2018, 18, 19, 19txunii 23089 . . . . . . . . . . . . . . 15 ((0[,]1) Γ— (0[,]1)) = βˆͺ (II Γ—t II)
2120, 1cnf 22742 . . . . . . . . . . . . . 14 (𝐴 ∈ ((II Γ—t II) Cn 𝐢) β†’ 𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡)
2217, 21syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡)
23 0elunit 13443 . . . . . . . . . . . . . 14 0 ∈ (0[,]1)
24 opelxpi 5713 . . . . . . . . . . . . . 14 ((𝑠 ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) β†’ βŸ¨π‘ , 0⟩ ∈ ((0[,]1) Γ— (0[,]1)))
2523, 24mpan2 690 . . . . . . . . . . . . 13 (𝑠 ∈ (0[,]1) β†’ βŸ¨π‘ , 0⟩ ∈ ((0[,]1) Γ— (0[,]1)))
26 fvco3 6988 . . . . . . . . . . . . 13 ((𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡 ∧ βŸ¨π‘ , 0⟩ ∈ ((0[,]1) Γ— (0[,]1))) β†’ ((𝐹 ∘ 𝐴)β€˜βŸ¨π‘ , 0⟩) = (πΉβ€˜(π΄β€˜βŸ¨π‘ , 0⟩)))
2722, 25, 26syl2an 597 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ ((𝐹 ∘ 𝐴)β€˜βŸ¨π‘ , 0⟩) = (πΉβ€˜(π΄β€˜βŸ¨π‘ , 0⟩)))
28 cvmliftphtlem.c . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐹 ∘ 𝐴) = 𝐾)
2928adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (𝐹 ∘ 𝐴) = 𝐾)
3029fveq1d 6891 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ ((𝐹 ∘ 𝐴)β€˜βŸ¨π‘ , 0⟩) = (πΎβ€˜βŸ¨π‘ , 0⟩))
3127, 30eqtr3d 2775 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(π΄β€˜βŸ¨π‘ , 0⟩)) = (πΎβ€˜βŸ¨π‘ , 0⟩))
32 df-ov 7409 . . . . . . . . . . . 12 (𝑠𝐴0) = (π΄β€˜βŸ¨π‘ , 0⟩)
3332fveq2i 6892 . . . . . . . . . . 11 (πΉβ€˜(𝑠𝐴0)) = (πΉβ€˜(π΄β€˜βŸ¨π‘ , 0⟩))
34 df-ov 7409 . . . . . . . . . . 11 (𝑠𝐾0) = (πΎβ€˜βŸ¨π‘ , 0⟩)
3531, 33, 343eqtr4g 2798 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(𝑠𝐴0)) = (𝑠𝐾0))
36 iitopon 24387 . . . . . . . . . . . . 13 II ∈ (TopOnβ€˜(0[,]1))
3736a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ II ∈ (TopOnβ€˜(0[,]1)))
384, 10phtpyhtpy 24490 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐺(PHtpyβ€˜π½)𝐻) βŠ† (𝐺(II Htpy 𝐽)𝐻))
3938, 11sseldd 3983 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐾 ∈ (𝐺(II Htpy 𝐽)𝐻))
4037, 4, 10, 39htpyi 24482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ ((𝑠𝐾0) = (πΊβ€˜π‘ ) ∧ (𝑠𝐾1) = (π»β€˜π‘ )))
4140simpld 496 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (𝑠𝐾0) = (πΊβ€˜π‘ ))
4235, 41eqtrd 2773 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(𝑠𝐴0)) = (πΊβ€˜π‘ ))
4342mpteq2dva 5248 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(𝑠𝐴0))) = (𝑠 ∈ (0[,]1) ↦ (πΊβ€˜π‘ )))
44 fovcdm 7574 . . . . . . . . . . 11 ((𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡 ∧ 𝑠 ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) β†’ (𝑠𝐴0) ∈ 𝐡)
4523, 44mp3an3 1451 . . . . . . . . . 10 ((𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡 ∧ 𝑠 ∈ (0[,]1)) β†’ (𝑠𝐴0) ∈ 𝐡)
4622, 45sylan 581 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (𝑠𝐴0) ∈ 𝐡)
47 eqidd 2734 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)))
48 cvmcn 34242 . . . . . . . . . . . 12 (𝐹 ∈ (𝐢 CovMap 𝐽) β†’ 𝐹 ∈ (𝐢 Cn 𝐽))
493, 48syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐹 ∈ (𝐢 Cn 𝐽))
50 eqid 2733 . . . . . . . . . . . 12 βˆͺ 𝐽 = βˆͺ 𝐽
511, 50cnf 22742 . . . . . . . . . . 11 (𝐹 ∈ (𝐢 Cn 𝐽) β†’ 𝐹:𝐡⟢βˆͺ 𝐽)
5249, 51syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:𝐡⟢βˆͺ 𝐽)
5352feqmptd 6958 . . . . . . . . 9 (πœ‘ β†’ 𝐹 = (π‘₯ ∈ 𝐡 ↦ (πΉβ€˜π‘₯)))
54 fveq2 6889 . . . . . . . . 9 (π‘₯ = (𝑠𝐴0) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜(𝑠𝐴0)))
5546, 47, 53, 54fmptco 7124 . . . . . . . 8 (πœ‘ β†’ (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))) = (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(𝑠𝐴0))))
5619, 50cnf 22742 . . . . . . . . . 10 (𝐺 ∈ (II Cn 𝐽) β†’ 𝐺:(0[,]1)⟢βˆͺ 𝐽)
574, 56syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐺:(0[,]1)⟢βˆͺ 𝐽)
5857feqmptd 6958 . . . . . . . 8 (πœ‘ β†’ 𝐺 = (𝑠 ∈ (0[,]1) ↦ (πΊβ€˜π‘ )))
5943, 55, 583eqtr4d 2783 . . . . . . 7 (πœ‘ β†’ (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))) = 𝐺)
60 cvmliftphtlem.0 . . . . . . 7 (πœ‘ β†’ (0𝐴0) = 𝑃)
6137cnmptid 23157 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ 𝑠) ∈ (II Cn II))
6223a1i 11 . . . . . . . . . 10 (πœ‘ β†’ 0 ∈ (0[,]1))
6337, 37, 62cnmptc 23158 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ 0) ∈ (II Cn II))
6437, 61, 63, 17cnmpt12f 23162 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) ∈ (II Cn 𝐢))
651cvmlift 34279 . . . . . . . . 9 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐡 ∧ (πΉβ€˜π‘ƒ) = (πΊβ€˜0))) β†’ βˆƒ!𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐺 ∧ (π‘“β€˜0) = 𝑃))
663, 4, 5, 6, 65syl22anc 838 . . . . . . . 8 (πœ‘ β†’ βˆƒ!𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐺 ∧ (π‘“β€˜0) = 𝑃))
67 coeq2 5857 . . . . . . . . . . 11 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) β†’ (𝐹 ∘ 𝑓) = (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))))
6867eqeq1d 2735 . . . . . . . . . 10 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) β†’ ((𝐹 ∘ 𝑓) = 𝐺 ↔ (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))) = 𝐺))
69 fveq1 6888 . . . . . . . . . . . 12 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) β†’ (π‘“β€˜0) = ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))β€˜0))
70 oveq1 7413 . . . . . . . . . . . . . 14 (𝑠 = 0 β†’ (𝑠𝐴0) = (0𝐴0))
71 eqid 2733 . . . . . . . . . . . . . 14 (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))
72 ovex 7439 . . . . . . . . . . . . . 14 (0𝐴0) ∈ V
7370, 71, 72fvmpt 6996 . . . . . . . . . . . . 13 (0 ∈ (0[,]1) β†’ ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))β€˜0) = (0𝐴0))
7423, 73ax-mp 5 . . . . . . . . . . . 12 ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))β€˜0) = (0𝐴0)
7569, 74eqtrdi 2789 . . . . . . . . . . 11 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) β†’ (π‘“β€˜0) = (0𝐴0))
7675eqeq1d 2735 . . . . . . . . . 10 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) β†’ ((π‘“β€˜0) = 𝑃 ↔ (0𝐴0) = 𝑃))
7768, 76anbi12d 632 . . . . . . . . 9 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) β†’ (((𝐹 ∘ 𝑓) = 𝐺 ∧ (π‘“β€˜0) = 𝑃) ↔ ((𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))) = 𝐺 ∧ (0𝐴0) = 𝑃)))
7877riota2 7388 . . . . . . . 8 (((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) ∈ (II Cn 𝐢) ∧ βˆƒ!𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐺 ∧ (π‘“β€˜0) = 𝑃)) β†’ (((𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))) = 𝐺 ∧ (0𝐴0) = 𝑃) ↔ (℩𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐺 ∧ (π‘“β€˜0) = 𝑃)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))))
7964, 66, 78syl2anc 585 . . . . . . 7 (πœ‘ β†’ (((𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))) = 𝐺 ∧ (0𝐴0) = 𝑃) ↔ (℩𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐺 ∧ (π‘“β€˜0) = 𝑃)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))))
8059, 60, 79mpbi2and 711 . . . . . 6 (πœ‘ β†’ (℩𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐺 ∧ (π‘“β€˜0) = 𝑃)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)))
812, 80eqtrid 2785 . . . . 5 (πœ‘ β†’ 𝑀 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)))
8219, 1cnf 22742 . . . . . . 7 (𝑀 ∈ (II Cn 𝐢) β†’ 𝑀:(0[,]1)⟢𝐡)
838, 82syl 17 . . . . . 6 (πœ‘ β†’ 𝑀:(0[,]1)⟢𝐡)
8483feqmptd 6958 . . . . 5 (πœ‘ β†’ 𝑀 = (𝑠 ∈ (0[,]1) ↦ (π‘€β€˜π‘ )))
8581, 84eqtr3d 2775 . . . 4 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) = (𝑠 ∈ (0[,]1) ↦ (π‘€β€˜π‘ )))
86 mpteqb 7015 . . . . 5 (βˆ€π‘  ∈ (0[,]1)(𝑠𝐴0) ∈ V β†’ ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) = (𝑠 ∈ (0[,]1) ↦ (π‘€β€˜π‘ )) ↔ βˆ€π‘  ∈ (0[,]1)(𝑠𝐴0) = (π‘€β€˜π‘ )))
87 ovexd 7441 . . . . 5 (𝑠 ∈ (0[,]1) β†’ (𝑠𝐴0) ∈ V)
8886, 87mprg 3068 . . . 4 ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) = (𝑠 ∈ (0[,]1) ↦ (π‘€β€˜π‘ )) ↔ βˆ€π‘  ∈ (0[,]1)(𝑠𝐴0) = (π‘€β€˜π‘ ))
8985, 88sylib 217 . . 3 (πœ‘ β†’ βˆ€π‘  ∈ (0[,]1)(𝑠𝐴0) = (π‘€β€˜π‘ ))
9089r19.21bi 3249 . 2 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (𝑠𝐴0) = (π‘€β€˜π‘ ))
91 1elunit 13444 . . . . . . . . . . . . . 14 1 ∈ (0[,]1)
92 opelxpi 5713 . . . . . . . . . . . . . 14 ((𝑠 ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) β†’ βŸ¨π‘ , 1⟩ ∈ ((0[,]1) Γ— (0[,]1)))
9391, 92mpan2 690 . . . . . . . . . . . . 13 (𝑠 ∈ (0[,]1) β†’ βŸ¨π‘ , 1⟩ ∈ ((0[,]1) Γ— (0[,]1)))
94 fvco3 6988 . . . . . . . . . . . . 13 ((𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡 ∧ βŸ¨π‘ , 1⟩ ∈ ((0[,]1) Γ— (0[,]1))) β†’ ((𝐹 ∘ 𝐴)β€˜βŸ¨π‘ , 1⟩) = (πΉβ€˜(π΄β€˜βŸ¨π‘ , 1⟩)))
9522, 93, 94syl2an 597 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ ((𝐹 ∘ 𝐴)β€˜βŸ¨π‘ , 1⟩) = (πΉβ€˜(π΄β€˜βŸ¨π‘ , 1⟩)))
9629fveq1d 6891 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ ((𝐹 ∘ 𝐴)β€˜βŸ¨π‘ , 1⟩) = (πΎβ€˜βŸ¨π‘ , 1⟩))
9795, 96eqtr3d 2775 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(π΄β€˜βŸ¨π‘ , 1⟩)) = (πΎβ€˜βŸ¨π‘ , 1⟩))
98 df-ov 7409 . . . . . . . . . . . 12 (𝑠𝐴1) = (π΄β€˜βŸ¨π‘ , 1⟩)
9998fveq2i 6892 . . . . . . . . . . 11 (πΉβ€˜(𝑠𝐴1)) = (πΉβ€˜(π΄β€˜βŸ¨π‘ , 1⟩))
100 df-ov 7409 . . . . . . . . . . 11 (𝑠𝐾1) = (πΎβ€˜βŸ¨π‘ , 1⟩)
10197, 99, 1003eqtr4g 2798 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(𝑠𝐴1)) = (𝑠𝐾1))
10240simprd 497 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (𝑠𝐾1) = (π»β€˜π‘ ))
103101, 102eqtrd 2773 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(𝑠𝐴1)) = (π»β€˜π‘ ))
104103mpteq2dva 5248 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(𝑠𝐴1))) = (𝑠 ∈ (0[,]1) ↦ (π»β€˜π‘ )))
105 fovcdm 7574 . . . . . . . . . . 11 ((𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡 ∧ 𝑠 ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) β†’ (𝑠𝐴1) ∈ 𝐡)
10691, 105mp3an3 1451 . . . . . . . . . 10 ((𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡 ∧ 𝑠 ∈ (0[,]1)) β†’ (𝑠𝐴1) ∈ 𝐡)
10722, 106sylan 581 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (𝑠𝐴1) ∈ 𝐡)
108 eqidd 2734 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)))
109 fveq2 6889 . . . . . . . . 9 (π‘₯ = (𝑠𝐴1) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜(𝑠𝐴1)))
110107, 108, 53, 109fmptco 7124 . . . . . . . 8 (πœ‘ β†’ (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))) = (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(𝑠𝐴1))))
11119, 50cnf 22742 . . . . . . . . . 10 (𝐻 ∈ (II Cn 𝐽) β†’ 𝐻:(0[,]1)⟢βˆͺ 𝐽)
11210, 111syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐻:(0[,]1)⟢βˆͺ 𝐽)
113112feqmptd 6958 . . . . . . . 8 (πœ‘ β†’ 𝐻 = (𝑠 ∈ (0[,]1) ↦ (π»β€˜π‘ )))
114104, 110, 1133eqtr4d 2783 . . . . . . 7 (πœ‘ β†’ (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))) = 𝐻)
115 iiconn 24395 . . . . . . . . . . . . 13 II ∈ Conn
116115a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ II ∈ Conn)
117 iinllyconn 34234 . . . . . . . . . . . . 13 II ∈ 𝑛-Locally Conn
118117a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ II ∈ 𝑛-Locally Conn)
11937, 63, 61, 17cnmpt12f 23162 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) ∈ (II Cn 𝐢))
120 cvmtop1 34240 . . . . . . . . . . . . . . 15 (𝐹 ∈ (𝐢 CovMap 𝐽) β†’ 𝐢 ∈ Top)
1213, 120syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐢 ∈ Top)
1221toptopon 22411 . . . . . . . . . . . . . 14 (𝐢 ∈ Top ↔ 𝐢 ∈ (TopOnβ€˜π΅))
123121, 122sylib 217 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐢 ∈ (TopOnβ€˜π΅))
124 ffvelcdm 7081 . . . . . . . . . . . . . 14 ((𝑀:(0[,]1)⟢𝐡 ∧ 0 ∈ (0[,]1)) β†’ (π‘€β€˜0) ∈ 𝐡)
12583, 23, 124sylancl 587 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘€β€˜0) ∈ 𝐡)
126 cnconst2 22779 . . . . . . . . . . . . 13 ((II ∈ (TopOnβ€˜(0[,]1)) ∧ 𝐢 ∈ (TopOnβ€˜π΅) ∧ (π‘€β€˜0) ∈ 𝐡) β†’ ((0[,]1) Γ— {(π‘€β€˜0)}) ∈ (II Cn 𝐢))
12737, 123, 125, 126syl3anc 1372 . . . . . . . . . . . 12 (πœ‘ β†’ ((0[,]1) Γ— {(π‘€β€˜0)}) ∈ (II Cn 𝐢))
1284, 10, 11phtpyi 24492 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ ((0𝐾𝑠) = (πΊβ€˜0) ∧ (1𝐾𝑠) = (πΊβ€˜1)))
129128simpld 496 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (0𝐾𝑠) = (πΊβ€˜0))
130 opelxpi 5713 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) β†’ ⟨0, π‘ βŸ© ∈ ((0[,]1) Γ— (0[,]1)))
13123, 130mpan 689 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (0[,]1) β†’ ⟨0, π‘ βŸ© ∈ ((0[,]1) Γ— (0[,]1)))
132 fvco3 6988 . . . . . . . . . . . . . . . . . . 19 ((𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡 ∧ ⟨0, π‘ βŸ© ∈ ((0[,]1) Γ— (0[,]1))) β†’ ((𝐹 ∘ 𝐴)β€˜βŸ¨0, π‘ βŸ©) = (πΉβ€˜(π΄β€˜βŸ¨0, π‘ βŸ©)))
13322, 131, 132syl2an 597 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ ((𝐹 ∘ 𝐴)β€˜βŸ¨0, π‘ βŸ©) = (πΉβ€˜(π΄β€˜βŸ¨0, π‘ βŸ©)))
13429fveq1d 6891 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ ((𝐹 ∘ 𝐴)β€˜βŸ¨0, π‘ βŸ©) = (πΎβ€˜βŸ¨0, π‘ βŸ©))
135133, 134eqtr3d 2775 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(π΄β€˜βŸ¨0, π‘ βŸ©)) = (πΎβ€˜βŸ¨0, π‘ βŸ©))
136 df-ov 7409 . . . . . . . . . . . . . . . . . 18 (0𝐴𝑠) = (π΄β€˜βŸ¨0, π‘ βŸ©)
137136fveq2i 6892 . . . . . . . . . . . . . . . . 17 (πΉβ€˜(0𝐴𝑠)) = (πΉβ€˜(π΄β€˜βŸ¨0, π‘ βŸ©))
138 df-ov 7409 . . . . . . . . . . . . . . . . 17 (0𝐾𝑠) = (πΎβ€˜βŸ¨0, π‘ βŸ©)
139135, 137, 1383eqtr4g 2798 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(0𝐴𝑠)) = (0𝐾𝑠))
1407simp3d 1145 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘€β€˜0) = 𝑃)
141140adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (π‘€β€˜0) = 𝑃)
142141fveq2d 6893 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(π‘€β€˜0)) = (πΉβ€˜π‘ƒ))
1436adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜π‘ƒ) = (πΊβ€˜0))
144142, 143eqtrd 2773 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(π‘€β€˜0)) = (πΊβ€˜0))
145129, 139, 1443eqtr4d 2783 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(0𝐴𝑠)) = (πΉβ€˜(π‘€β€˜0)))
146145mpteq2dva 5248 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(0𝐴𝑠))) = (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(π‘€β€˜0))))
147 fconstmpt 5737 . . . . . . . . . . . . . 14 ((0[,]1) Γ— {(πΉβ€˜(π‘€β€˜0))}) = (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(π‘€β€˜0)))
148146, 147eqtr4di 2791 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(0𝐴𝑠))) = ((0[,]1) Γ— {(πΉβ€˜(π‘€β€˜0))}))
149 fovcdm 7574 . . . . . . . . . . . . . . . 16 ((𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡 ∧ 0 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) β†’ (0𝐴𝑠) ∈ 𝐡)
15023, 149mp3an2 1450 . . . . . . . . . . . . . . 15 ((𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡 ∧ 𝑠 ∈ (0[,]1)) β†’ (0𝐴𝑠) ∈ 𝐡)
15122, 150sylan 581 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (0𝐴𝑠) ∈ 𝐡)
152 eqidd 2734 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)))
153 fveq2 6889 . . . . . . . . . . . . . 14 (π‘₯ = (0𝐴𝑠) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜(0𝐴𝑠)))
154151, 152, 53, 153fmptco 7124 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠))) = (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(0𝐴𝑠))))
15552ffnd 6716 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐹 Fn 𝐡)
156 fcoconst 7129 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐡 ∧ (π‘€β€˜0) ∈ 𝐡) β†’ (𝐹 ∘ ((0[,]1) Γ— {(π‘€β€˜0)})) = ((0[,]1) Γ— {(πΉβ€˜(π‘€β€˜0))}))
157155, 125, 156syl2anc 585 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐹 ∘ ((0[,]1) Γ— {(π‘€β€˜0)})) = ((0[,]1) Γ— {(πΉβ€˜(π‘€β€˜0))}))
158148, 154, 1573eqtr4d 2783 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠))) = (𝐹 ∘ ((0[,]1) Γ— {(π‘€β€˜0)})))
15960, 140eqtr4d 2776 . . . . . . . . . . . . 13 (πœ‘ β†’ (0𝐴0) = (π‘€β€˜0))
160 oveq2 7414 . . . . . . . . . . . . . . 15 (𝑠 = 0 β†’ (0𝐴𝑠) = (0𝐴0))
161 eqid 2733 . . . . . . . . . . . . . . 15 (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠))
162160, 161, 72fvmpt 6996 . . . . . . . . . . . . . 14 (0 ∈ (0[,]1) β†’ ((𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠))β€˜0) = (0𝐴0))
16323, 162ax-mp 5 . . . . . . . . . . . . 13 ((𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠))β€˜0) = (0𝐴0)
164 fvex 6902 . . . . . . . . . . . . . . 15 (π‘€β€˜0) ∈ V
165164fvconst2 7202 . . . . . . . . . . . . . 14 (0 ∈ (0[,]1) β†’ (((0[,]1) Γ— {(π‘€β€˜0)})β€˜0) = (π‘€β€˜0))
16623, 165ax-mp 5 . . . . . . . . . . . . 13 (((0[,]1) Γ— {(π‘€β€˜0)})β€˜0) = (π‘€β€˜0)
167159, 163, 1663eqtr4g 2798 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠))β€˜0) = (((0[,]1) Γ— {(π‘€β€˜0)})β€˜0))
1681, 19, 3, 116, 118, 62, 119, 127, 158, 167cvmliftmoi 34263 . . . . . . . . . . 11 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) = ((0[,]1) Γ— {(π‘€β€˜0)}))
169 fconstmpt 5737 . . . . . . . . . . 11 ((0[,]1) Γ— {(π‘€β€˜0)}) = (𝑠 ∈ (0[,]1) ↦ (π‘€β€˜0))
170168, 169eqtrdi 2789 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (π‘€β€˜0)))
171 mpteqb 7015 . . . . . . . . . . 11 (βˆ€π‘  ∈ (0[,]1)(0𝐴𝑠) ∈ V β†’ ((𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (π‘€β€˜0)) ↔ βˆ€π‘  ∈ (0[,]1)(0𝐴𝑠) = (π‘€β€˜0)))
172 ovexd 7441 . . . . . . . . . . 11 (𝑠 ∈ (0[,]1) β†’ (0𝐴𝑠) ∈ V)
173171, 172mprg 3068 . . . . . . . . . 10 ((𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (π‘€β€˜0)) ↔ βˆ€π‘  ∈ (0[,]1)(0𝐴𝑠) = (π‘€β€˜0))
174170, 173sylib 217 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘  ∈ (0[,]1)(0𝐴𝑠) = (π‘€β€˜0))
175 oveq2 7414 . . . . . . . . . . 11 (𝑠 = 1 β†’ (0𝐴𝑠) = (0𝐴1))
176175eqeq1d 2735 . . . . . . . . . 10 (𝑠 = 1 β†’ ((0𝐴𝑠) = (π‘€β€˜0) ↔ (0𝐴1) = (π‘€β€˜0)))
177176rspcv 3609 . . . . . . . . 9 (1 ∈ (0[,]1) β†’ (βˆ€π‘  ∈ (0[,]1)(0𝐴𝑠) = (π‘€β€˜0) β†’ (0𝐴1) = (π‘€β€˜0)))
17891, 174, 177mpsyl 68 . . . . . . . 8 (πœ‘ β†’ (0𝐴1) = (π‘€β€˜0))
179178, 140eqtrd 2773 . . . . . . 7 (πœ‘ β†’ (0𝐴1) = 𝑃)
18091a1i 11 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ (0[,]1))
18137, 37, 180cnmptc 23158 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ 1) ∈ (II Cn II))
18237, 61, 181, 17cnmpt12f 23162 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) ∈ (II Cn 𝐢))
1831cvmlift 34279 . . . . . . . . 9 (((𝐹 ∈ (𝐢 CovMap 𝐽) ∧ 𝐻 ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐡 ∧ (πΉβ€˜π‘ƒ) = (π»β€˜0))) β†’ βˆƒ!𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐻 ∧ (π‘“β€˜0) = 𝑃))
1843, 10, 5, 14, 183syl22anc 838 . . . . . . . 8 (πœ‘ β†’ βˆƒ!𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐻 ∧ (π‘“β€˜0) = 𝑃))
185 coeq2 5857 . . . . . . . . . . 11 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) β†’ (𝐹 ∘ 𝑓) = (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))))
186185eqeq1d 2735 . . . . . . . . . 10 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) β†’ ((𝐹 ∘ 𝑓) = 𝐻 ↔ (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))) = 𝐻))
187 fveq1 6888 . . . . . . . . . . . 12 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) β†’ (π‘“β€˜0) = ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))β€˜0))
188 oveq1 7413 . . . . . . . . . . . . . 14 (𝑠 = 0 β†’ (𝑠𝐴1) = (0𝐴1))
189 eqid 2733 . . . . . . . . . . . . . 14 (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))
190 ovex 7439 . . . . . . . . . . . . . 14 (0𝐴1) ∈ V
191188, 189, 190fvmpt 6996 . . . . . . . . . . . . 13 (0 ∈ (0[,]1) β†’ ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))β€˜0) = (0𝐴1))
19223, 191ax-mp 5 . . . . . . . . . . . 12 ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))β€˜0) = (0𝐴1)
193187, 192eqtrdi 2789 . . . . . . . . . . 11 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) β†’ (π‘“β€˜0) = (0𝐴1))
194193eqeq1d 2735 . . . . . . . . . 10 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) β†’ ((π‘“β€˜0) = 𝑃 ↔ (0𝐴1) = 𝑃))
195186, 194anbi12d 632 . . . . . . . . 9 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) β†’ (((𝐹 ∘ 𝑓) = 𝐻 ∧ (π‘“β€˜0) = 𝑃) ↔ ((𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))) = 𝐻 ∧ (0𝐴1) = 𝑃)))
196195riota2 7388 . . . . . . . 8 (((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) ∈ (II Cn 𝐢) ∧ βˆƒ!𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐻 ∧ (π‘“β€˜0) = 𝑃)) β†’ (((𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))) = 𝐻 ∧ (0𝐴1) = 𝑃) ↔ (℩𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐻 ∧ (π‘“β€˜0) = 𝑃)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))))
197182, 184, 196syl2anc 585 . . . . . . 7 (πœ‘ β†’ (((𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))) = 𝐻 ∧ (0𝐴1) = 𝑃) ↔ (℩𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐻 ∧ (π‘“β€˜0) = 𝑃)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))))
198114, 179, 197mpbi2and 711 . . . . . 6 (πœ‘ β†’ (℩𝑓 ∈ (II Cn 𝐢)((𝐹 ∘ 𝑓) = 𝐻 ∧ (π‘“β€˜0) = 𝑃)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)))
1999, 198eqtrid 2785 . . . . 5 (πœ‘ β†’ 𝑁 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)))
20019, 1cnf 22742 . . . . . . 7 (𝑁 ∈ (II Cn 𝐢) β†’ 𝑁:(0[,]1)⟢𝐡)
20116, 200syl 17 . . . . . 6 (πœ‘ β†’ 𝑁:(0[,]1)⟢𝐡)
202201feqmptd 6958 . . . . 5 (πœ‘ β†’ 𝑁 = (𝑠 ∈ (0[,]1) ↦ (π‘β€˜π‘ )))
203199, 202eqtr3d 2775 . . . 4 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) = (𝑠 ∈ (0[,]1) ↦ (π‘β€˜π‘ )))
204 mpteqb 7015 . . . . 5 (βˆ€π‘  ∈ (0[,]1)(𝑠𝐴1) ∈ V β†’ ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) = (𝑠 ∈ (0[,]1) ↦ (π‘β€˜π‘ )) ↔ βˆ€π‘  ∈ (0[,]1)(𝑠𝐴1) = (π‘β€˜π‘ )))
205 ovexd 7441 . . . . 5 (𝑠 ∈ (0[,]1) β†’ (𝑠𝐴1) ∈ V)
206204, 205mprg 3068 . . . 4 ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) = (𝑠 ∈ (0[,]1) ↦ (π‘β€˜π‘ )) ↔ βˆ€π‘  ∈ (0[,]1)(𝑠𝐴1) = (π‘β€˜π‘ ))
207203, 206sylib 217 . . 3 (πœ‘ β†’ βˆ€π‘  ∈ (0[,]1)(𝑠𝐴1) = (π‘β€˜π‘ ))
208207r19.21bi 3249 . 2 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (𝑠𝐴1) = (π‘β€˜π‘ ))
209174r19.21bi 3249 . 2 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (0𝐴𝑠) = (π‘€β€˜0))
21037, 181, 61, 17cnmpt12f 23162 . . . . . 6 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) ∈ (II Cn 𝐢))
211 ffvelcdm 7081 . . . . . . . 8 ((𝑀:(0[,]1)⟢𝐡 ∧ 1 ∈ (0[,]1)) β†’ (π‘€β€˜1) ∈ 𝐡)
21283, 91, 211sylancl 587 . . . . . . 7 (πœ‘ β†’ (π‘€β€˜1) ∈ 𝐡)
213 cnconst2 22779 . . . . . . 7 ((II ∈ (TopOnβ€˜(0[,]1)) ∧ 𝐢 ∈ (TopOnβ€˜π΅) ∧ (π‘€β€˜1) ∈ 𝐡) β†’ ((0[,]1) Γ— {(π‘€β€˜1)}) ∈ (II Cn 𝐢))
21437, 123, 212, 213syl3anc 1372 . . . . . 6 (πœ‘ β†’ ((0[,]1) Γ— {(π‘€β€˜1)}) ∈ (II Cn 𝐢))
215 opelxpi 5713 . . . . . . . . . . . . . 14 ((1 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) β†’ ⟨1, π‘ βŸ© ∈ ((0[,]1) Γ— (0[,]1)))
21691, 215mpan 689 . . . . . . . . . . . . 13 (𝑠 ∈ (0[,]1) β†’ ⟨1, π‘ βŸ© ∈ ((0[,]1) Γ— (0[,]1)))
217 fvco3 6988 . . . . . . . . . . . . 13 ((𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡 ∧ ⟨1, π‘ βŸ© ∈ ((0[,]1) Γ— (0[,]1))) β†’ ((𝐹 ∘ 𝐴)β€˜βŸ¨1, π‘ βŸ©) = (πΉβ€˜(π΄β€˜βŸ¨1, π‘ βŸ©)))
21822, 216, 217syl2an 597 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ ((𝐹 ∘ 𝐴)β€˜βŸ¨1, π‘ βŸ©) = (πΉβ€˜(π΄β€˜βŸ¨1, π‘ βŸ©)))
21929fveq1d 6891 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ ((𝐹 ∘ 𝐴)β€˜βŸ¨1, π‘ βŸ©) = (πΎβ€˜βŸ¨1, π‘ βŸ©))
220218, 219eqtr3d 2775 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(π΄β€˜βŸ¨1, π‘ βŸ©)) = (πΎβ€˜βŸ¨1, π‘ βŸ©))
221 df-ov 7409 . . . . . . . . . . . 12 (1𝐴𝑠) = (π΄β€˜βŸ¨1, π‘ βŸ©)
222221fveq2i 6892 . . . . . . . . . . 11 (πΉβ€˜(1𝐴𝑠)) = (πΉβ€˜(π΄β€˜βŸ¨1, π‘ βŸ©))
223 df-ov 7409 . . . . . . . . . . 11 (1𝐾𝑠) = (πΎβ€˜βŸ¨1, π‘ βŸ©)
224220, 222, 2233eqtr4g 2798 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(1𝐴𝑠)) = (1𝐾𝑠))
225128simprd 497 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (1𝐾𝑠) = (πΊβ€˜1))
2267simp2d 1144 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐹 ∘ 𝑀) = 𝐺)
227226adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (𝐹 ∘ 𝑀) = 𝐺)
228227fveq1d 6891 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ ((𝐹 ∘ 𝑀)β€˜1) = (πΊβ€˜1))
22983adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ 𝑀:(0[,]1)⟢𝐡)
230 fvco3 6988 . . . . . . . . . . . 12 ((𝑀:(0[,]1)⟢𝐡 ∧ 1 ∈ (0[,]1)) β†’ ((𝐹 ∘ 𝑀)β€˜1) = (πΉβ€˜(π‘€β€˜1)))
231229, 91, 230sylancl 587 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ ((𝐹 ∘ 𝑀)β€˜1) = (πΉβ€˜(π‘€β€˜1)))
232228, 231eqtr3d 2775 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΊβ€˜1) = (πΉβ€˜(π‘€β€˜1)))
233224, 225, 2323eqtrd 2777 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (πΉβ€˜(1𝐴𝑠)) = (πΉβ€˜(π‘€β€˜1)))
234233mpteq2dva 5248 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(1𝐴𝑠))) = (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(π‘€β€˜1))))
235 fconstmpt 5737 . . . . . . . 8 ((0[,]1) Γ— {(πΉβ€˜(π‘€β€˜1))}) = (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(π‘€β€˜1)))
236234, 235eqtr4di 2791 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(1𝐴𝑠))) = ((0[,]1) Γ— {(πΉβ€˜(π‘€β€˜1))}))
237 fovcdm 7574 . . . . . . . . . 10 ((𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡 ∧ 1 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) β†’ (1𝐴𝑠) ∈ 𝐡)
23891, 237mp3an2 1450 . . . . . . . . 9 ((𝐴:((0[,]1) Γ— (0[,]1))⟢𝐡 ∧ 𝑠 ∈ (0[,]1)) β†’ (1𝐴𝑠) ∈ 𝐡)
23922, 238sylan 581 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (1𝐴𝑠) ∈ 𝐡)
240 eqidd 2734 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)))
241 fveq2 6889 . . . . . . . 8 (π‘₯ = (1𝐴𝑠) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜(1𝐴𝑠)))
242239, 240, 53, 241fmptco 7124 . . . . . . 7 (πœ‘ β†’ (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠))) = (𝑠 ∈ (0[,]1) ↦ (πΉβ€˜(1𝐴𝑠))))
243 fcoconst 7129 . . . . . . . 8 ((𝐹 Fn 𝐡 ∧ (π‘€β€˜1) ∈ 𝐡) β†’ (𝐹 ∘ ((0[,]1) Γ— {(π‘€β€˜1)})) = ((0[,]1) Γ— {(πΉβ€˜(π‘€β€˜1))}))
244155, 212, 243syl2anc 585 . . . . . . 7 (πœ‘ β†’ (𝐹 ∘ ((0[,]1) Γ— {(π‘€β€˜1)})) = ((0[,]1) Γ— {(πΉβ€˜(π‘€β€˜1))}))
245236, 242, 2443eqtr4d 2783 . . . . . 6 (πœ‘ β†’ (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠))) = (𝐹 ∘ ((0[,]1) Γ— {(π‘€β€˜1)})))
246 oveq1 7413 . . . . . . . . . 10 (𝑠 = 1 β†’ (𝑠𝐴0) = (1𝐴0))
247 fveq2 6889 . . . . . . . . . 10 (𝑠 = 1 β†’ (π‘€β€˜π‘ ) = (π‘€β€˜1))
248246, 247eqeq12d 2749 . . . . . . . . 9 (𝑠 = 1 β†’ ((𝑠𝐴0) = (π‘€β€˜π‘ ) ↔ (1𝐴0) = (π‘€β€˜1)))
249248rspcv 3609 . . . . . . . 8 (1 ∈ (0[,]1) β†’ (βˆ€π‘  ∈ (0[,]1)(𝑠𝐴0) = (π‘€β€˜π‘ ) β†’ (1𝐴0) = (π‘€β€˜1)))
25091, 89, 249mpsyl 68 . . . . . . 7 (πœ‘ β†’ (1𝐴0) = (π‘€β€˜1))
251 oveq2 7414 . . . . . . . . 9 (𝑠 = 0 β†’ (1𝐴𝑠) = (1𝐴0))
252 eqid 2733 . . . . . . . . 9 (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠))
253 ovex 7439 . . . . . . . . 9 (1𝐴0) ∈ V
254251, 252, 253fvmpt 6996 . . . . . . . 8 (0 ∈ (0[,]1) β†’ ((𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠))β€˜0) = (1𝐴0))
25523, 254ax-mp 5 . . . . . . 7 ((𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠))β€˜0) = (1𝐴0)
256 fvex 6902 . . . . . . . . 9 (π‘€β€˜1) ∈ V
257256fvconst2 7202 . . . . . . . 8 (0 ∈ (0[,]1) β†’ (((0[,]1) Γ— {(π‘€β€˜1)})β€˜0) = (π‘€β€˜1))
25823, 257ax-mp 5 . . . . . . 7 (((0[,]1) Γ— {(π‘€β€˜1)})β€˜0) = (π‘€β€˜1)
259250, 255, 2583eqtr4g 2798 . . . . . 6 (πœ‘ β†’ ((𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠))β€˜0) = (((0[,]1) Γ— {(π‘€β€˜1)})β€˜0))
2601, 19, 3, 116, 118, 62, 210, 214, 245, 259cvmliftmoi 34263 . . . . 5 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) = ((0[,]1) Γ— {(π‘€β€˜1)}))
261 fconstmpt 5737 . . . . 5 ((0[,]1) Γ— {(π‘€β€˜1)}) = (𝑠 ∈ (0[,]1) ↦ (π‘€β€˜1))
262260, 261eqtrdi 2789 . . . 4 (πœ‘ β†’ (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (π‘€β€˜1)))
263 mpteqb 7015 . . . . 5 (βˆ€π‘  ∈ (0[,]1)(1𝐴𝑠) ∈ V β†’ ((𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (π‘€β€˜1)) ↔ βˆ€π‘  ∈ (0[,]1)(1𝐴𝑠) = (π‘€β€˜1)))
264 ovexd 7441 . . . . 5 (𝑠 ∈ (0[,]1) β†’ (1𝐴𝑠) ∈ V)
265263, 264mprg 3068 . . . 4 ((𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (π‘€β€˜1)) ↔ βˆ€π‘  ∈ (0[,]1)(1𝐴𝑠) = (π‘€β€˜1))
266262, 265sylib 217 . . 3 (πœ‘ β†’ βˆ€π‘  ∈ (0[,]1)(1𝐴𝑠) = (π‘€β€˜1))
267266r19.21bi 3249 . 2 ((πœ‘ ∧ 𝑠 ∈ (0[,]1)) β†’ (1𝐴𝑠) = (π‘€β€˜1))
2688, 16, 17, 90, 208, 209, 267isphtpy2d 24495 1 (πœ‘ β†’ 𝐴 ∈ (𝑀(PHtpyβ€˜πΆ)𝑁))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  βˆƒ!wreu 3375  Vcvv 3475  {csn 4628  βŸ¨cop 4634  βˆͺ cuni 4908   ↦ cmpt 5231   Γ— cxp 5674   ∘ ccom 5680   Fn wfn 6536  βŸΆwf 6537  β€˜cfv 6541  β„©crio 7361  (class class class)co 7406  0cc0 11107  1c1 11108  [,]cicc 13324  Topctop 22387  TopOnctopon 22404   Cn ccn 22720  Conncconn 22907  π‘›-Locally cnlly 22961   Γ—t ctx 23056  IIcii 24383   Htpy chtpy 24475  PHtpycphtpy 24476   CovMap ccvm 34235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185  ax-addf 11186  ax-mulf 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-of 7667  df-om 7853  df-1st 7972  df-2nd 7973  df-supp 8144  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-er 8700  df-ec 8702  df-map 8819  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-sum 15630  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-mulr 17208  df-starv 17209  df-sca 17210  df-vsca 17211  df-ip 17212  df-tset 17213  df-ple 17214  df-ds 17216  df-unif 17217  df-hom 17218  df-cco 17219  df-rest 17365  df-topn 17366  df-0g 17384  df-gsum 17385  df-topgen 17386  df-pt 17387  df-prds 17390  df-xrs 17445  df-qtop 17450  df-imas 17451  df-xps 17453  df-mre 17527  df-mrc 17528  df-acs 17530  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-submnd 18669  df-mulg 18946  df-cntz 19176  df-cmn 19645  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-cnfld 20938  df-top 22388  df-topon 22405  df-topsp 22427  df-bases 22441  df-cld 22515  df-ntr 22516  df-cls 22517  df-nei 22594  df-cn 22723  df-cnp 22724  df-cmp 22883  df-conn 22908  df-lly 22962  df-nlly 22963  df-tx 23058  df-hmeo 23251  df-xms 23818  df-ms 23819  df-tms 23820  df-ii 24385  df-htpy 24478  df-phtpy 24479  df-phtpc 24500  df-pconn 34201  df-sconn 34202  df-cvm 34236
This theorem is referenced by:  cvmliftpht  34298
  Copyright terms: Public domain W3C validator