Metamath Proof Explorer

Theorem cvmliftphtlem

Description: Lemma for cvmliftpht . (Contributed by Mario Carneiro, 6-Jul-2015)

Ref Expression
Hypotheses 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 cvmliftphtlem ( 𝜑 → 𝐴 ∈ ( 𝑀 ( PHtpy ‘ 𝐶 ) 𝑁 ) )

Proof

Step Hyp Ref Expression
1 cvmliftpht.b ⊢ 𝐵 = ∪ 𝐶
2 cvmliftpht.m ⊢ 𝑀 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
3 cvmliftpht.n ⊢ 𝑁 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐻 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
4 cvmliftpht.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
5 cvmliftpht.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
6 cvmliftpht.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
7 cvmliftphtlem.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
8 cvmliftphtlem.h ⊢ ( 𝜑 → 𝐻 ∈ ( II Cn 𝐽 ) )
9 cvmliftphtlem.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) )
10 cvmliftphtlem.a ⊢ ( 𝜑 → 𝐴 ∈ ( ( II ×t II ) Cn 𝐶 ) )
11 cvmliftphtlem.c ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐴 ) = 𝐾 )
12 cvmliftphtlem.0 ⊢ ( 𝜑 → ( 0 𝐴 0 ) = 𝑃 )
13 1 2 4 7 5 6 cvmliftiota ⊢ ( 𝜑 → ( 𝑀 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝑀 ) = 𝐺 ∧ ( 𝑀 ‘ 0 ) = 𝑃 ) )
14 13 simp1d ⊢ ( 𝜑 → 𝑀 ∈ ( II Cn 𝐶 ) )
15 7 8 9 phtpy01 ⊢ ( 𝜑 → ( ( 𝐺 ‘ 0 ) = ( 𝐻 ‘ 0 ) ∧ ( 𝐺 ‘ 1 ) = ( 𝐻 ‘ 1 ) ) )
16 15 simpld ⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = ( 𝐻 ‘ 0 ) )
17 6 16 eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐻 ‘ 0 ) )
18 1 3 4 8 5 17 cvmliftiota ⊢ ( 𝜑 → ( 𝑁 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝑁 ) = 𝐻 ∧ ( 𝑁 ‘ 0 ) = 𝑃 ) )
19 18 simp1d ⊢ ( 𝜑 → 𝑁 ∈ ( II Cn 𝐶 ) )
20 iitop ⊢ II ∈ Top
21 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
22 20 20 21 21 txunii ⊢ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) = ∪ ( II ×t II )
23 22 1 cnf ⊢ ( 𝐴 ∈ ( ( II ×t II ) Cn 𝐶 ) → 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )
24 10 23 syl ⊢ ( 𝜑 → 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )
25 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
26 opelxpi ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ⟨ 𝑠 , 0 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
27 25 26 mpan2 ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ⟨ 𝑠 , 0 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
28 fvco3 ⊢ ( ( 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ ⟨ 𝑠 , 0 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( ( 𝐹 ∘ 𝐴 ) ‘ ⟨ 𝑠 , 0 ⟩ ) = ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 𝑠 , 0 ⟩ ) ) )
29 24 27 28 syl2an ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝐴 ) ‘ ⟨ 𝑠 , 0 ⟩ ) = ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 𝑠 , 0 ⟩ ) ) )
30 11 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ∘ 𝐴 ) = 𝐾 )
31 30 fveq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝐴 ) ‘ ⟨ 𝑠 , 0 ⟩ ) = ( 𝐾 ‘ ⟨ 𝑠 , 0 ⟩ ) )
32 29 31 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 𝑠 , 0 ⟩ ) ) = ( 𝐾 ‘ ⟨ 𝑠 , 0 ⟩ ) )
33 df-ov ⊢ ( 𝑠 𝐴 0 ) = ( 𝐴 ‘ ⟨ 𝑠 , 0 ⟩ )
34 33 fveq2i ⊢ ( 𝐹 ‘ ( 𝑠 𝐴 0 ) ) = ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 𝑠 , 0 ⟩ ) )
35 df-ov ⊢ ( 𝑠 𝐾 0 ) = ( 𝐾 ‘ ⟨ 𝑠 , 0 ⟩ )
36 32 34 35 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝑠 𝐴 0 ) ) = ( 𝑠 𝐾 0 ) )
37 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
38 37 a1i ⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
39 7 8 phtpyhtpy ⊢ ( 𝜑 → ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ⊆ ( 𝐺 ( II Htpy 𝐽 ) 𝐻 ) )
40 39 9 sseldd ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐺 ( II Htpy 𝐽 ) 𝐻 ) )
41 38 7 8 40 htpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑠 𝐾 0 ) = ( 𝐺 ‘ 𝑠 ) ∧ ( 𝑠 𝐾 1 ) = ( 𝐻 ‘ 𝑠 ) ) )
42 41 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐾 0 ) = ( 𝐺 ‘ 𝑠 ) )
43 36 42 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝑠 𝐴 0 ) ) = ( 𝐺 ‘ 𝑠 ) )
44 43 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 𝑠 𝐴 0 ) ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ 𝑠 ) ) )
45 fovrn ⊢ ( ( 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ 𝑠 ∈ ( 0 [,] 1 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐴 0 ) ∈ 𝐵 )
46 25 45 mp3an3 ⊢ ( ( 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐴 0 ) ∈ 𝐵 )
47 24 46 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐴 0 ) ∈ 𝐵 )
48 eqidd ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) )
49 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
50 4 49 syl ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
51 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
52 1 51 cnf ⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ ∪ 𝐽 )
53 50 52 syl ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ∪ 𝐽 )
54 53 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑥 ) ) )
55 fveq2 ⊢ ( 𝑥 = ( 𝑠 𝐴 0 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑠 𝐴 0 ) ) )
56 47 48 54 55 fmptco ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 𝑠 𝐴 0 ) ) ) )
57 21 51 cnf ⊢ ( 𝐺 ∈ ( II Cn 𝐽 ) → 𝐺 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
58 7 57 syl ⊢ ( 𝜑 → 𝐺 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
59 58 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ 𝑠 ) ) )
60 44 56 59 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ) = 𝐺 )
61 38 cnmptid ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ 𝑠 ) ∈ ( II Cn II ) )
62 25 a1i ⊢ ( 𝜑 → 0 ∈ ( 0 [,] 1 ) )
63 38 38 62 cnmptc ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ 0 ) ∈ ( II Cn II ) )
64 38 61 63 10 cnmpt12f ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ∈ ( II Cn 𝐶 ) )
65 1 cvmlift ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) ) ) → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
66 4 7 5 6 65 syl22anc ⊢ ( 𝜑 → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
67 coeq2 ⊢ ( 𝑓 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) → ( 𝐹 ∘ 𝑓 ) = ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ) )
68 67 eqeq1d ⊢ ( 𝑓 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) → ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ↔ ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ) = 𝐺 ) )
69 fveq1 ⊢ ( 𝑓 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) → ( 𝑓 ‘ 0 ) = ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ‘ 0 ) )
70 oveq1 ⊢ ( 𝑠 = 0 → ( 𝑠 𝐴 0 ) = ( 0 𝐴 0 ) )
71 eqid ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) )
72 ovex ⊢ ( 0 𝐴 0 ) ∈ V
73 70 71 72 fvmpt ⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ‘ 0 ) = ( 0 𝐴 0 ) )
74 25 73 ax-mp ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ‘ 0 ) = ( 0 𝐴 0 )
75 69 74 eqtrdi ⊢ ( 𝑓 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) → ( 𝑓 ‘ 0 ) = ( 0 𝐴 0 ) )
76 75 eqeq1d ⊢ ( 𝑓 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) → ( ( 𝑓 ‘ 0 ) = 𝑃 ↔ ( 0 𝐴 0 ) = 𝑃 ) )
77 68 76 anbi12d ⊢ ( 𝑓 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) → ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ) = 𝐺 ∧ ( 0 𝐴 0 ) = 𝑃 ) ) )
78 77 riota2 ⊢ ( ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ∈ ( II Cn 𝐶 ) ∧ ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) → ( ( ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ) = 𝐺 ∧ ( 0 𝐴 0 ) = 𝑃 ) ↔ ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ) )
79 64 66 78 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ) = 𝐺 ∧ ( 0 𝐴 0 ) = 𝑃 ) ↔ ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) ) )
80 60 12 79 mpbi2and ⊢ ( 𝜑 → ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) )
81 2 80 syl5eq ⊢ ( 𝜑 → 𝑀 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) )
82 21 1 cnf ⊢ ( 𝑀 ∈ ( II Cn 𝐶 ) → 𝑀 : ( 0 [,] 1 ) ⟶ 𝐵 )
83 14 82 syl ⊢ ( 𝜑 → 𝑀 : ( 0 [,] 1 ) ⟶ 𝐵 )
84 83 feqmptd ⊢ ( 𝜑 → 𝑀 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑀 ‘ 𝑠 ) ) )
85 81 84 eqtr3d ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑀 ‘ 𝑠 ) ) )
86 mpteqb ⊢ ( ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 𝑠 𝐴 0 ) ∈ V → ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑀 ‘ 𝑠 ) ) ↔ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 𝑠 𝐴 0 ) = ( 𝑀 ‘ 𝑠 ) ) )
87 ovexd ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ( 𝑠 𝐴 0 ) ∈ V )
88 86 87 mprg ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 0 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑀 ‘ 𝑠 ) ) ↔ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 𝑠 𝐴 0 ) = ( 𝑀 ‘ 𝑠 ) )
89 85 88 sylib ⊢ ( 𝜑 → ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 𝑠 𝐴 0 ) = ( 𝑀 ‘ 𝑠 ) )
90 89 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐴 0 ) = ( 𝑀 ‘ 𝑠 ) )
91 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
92 opelxpi ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 1 ∈ ( 0 [,] 1 ) ) → ⟨ 𝑠 , 1 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
93 91 92 mpan2 ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ⟨ 𝑠 , 1 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
94 fvco3 ⊢ ( ( 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ ⟨ 𝑠 , 1 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( ( 𝐹 ∘ 𝐴 ) ‘ ⟨ 𝑠 , 1 ⟩ ) = ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 𝑠 , 1 ⟩ ) ) )
95 24 93 94 syl2an ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝐴 ) ‘ ⟨ 𝑠 , 1 ⟩ ) = ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 𝑠 , 1 ⟩ ) ) )
96 30 fveq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝐴 ) ‘ ⟨ 𝑠 , 1 ⟩ ) = ( 𝐾 ‘ ⟨ 𝑠 , 1 ⟩ ) )
97 95 96 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 𝑠 , 1 ⟩ ) ) = ( 𝐾 ‘ ⟨ 𝑠 , 1 ⟩ ) )
98 df-ov ⊢ ( 𝑠 𝐴 1 ) = ( 𝐴 ‘ ⟨ 𝑠 , 1 ⟩ )
99 98 fveq2i ⊢ ( 𝐹 ‘ ( 𝑠 𝐴 1 ) ) = ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 𝑠 , 1 ⟩ ) )
100 df-ov ⊢ ( 𝑠 𝐾 1 ) = ( 𝐾 ‘ ⟨ 𝑠 , 1 ⟩ )
101 97 99 100 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝑠 𝐴 1 ) ) = ( 𝑠 𝐾 1 ) )
102 41 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐾 1 ) = ( 𝐻 ‘ 𝑠 ) )
103 101 102 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝑠 𝐴 1 ) ) = ( 𝐻 ‘ 𝑠 ) )
104 103 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 𝑠 𝐴 1 ) ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐻 ‘ 𝑠 ) ) )
105 fovrn ⊢ ( ( 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ 𝑠 ∈ ( 0 [,] 1 ) ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐴 1 ) ∈ 𝐵 )
106 91 105 mp3an3 ⊢ ( ( 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐴 1 ) ∈ 𝐵 )
107 24 106 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐴 1 ) ∈ 𝐵 )
108 eqidd ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) )
109 fveq2 ⊢ ( 𝑥 = ( 𝑠 𝐴 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑠 𝐴 1 ) ) )
110 107 108 54 109 fmptco ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 𝑠 𝐴 1 ) ) ) )
111 21 51 cnf ⊢ ( 𝐻 ∈ ( II Cn 𝐽 ) → 𝐻 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
112 8 111 syl ⊢ ( 𝜑 → 𝐻 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
113 112 feqmptd ⊢ ( 𝜑 → 𝐻 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐻 ‘ 𝑠 ) ) )
114 104 110 113 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ) = 𝐻 )
115 iiconn ⊢ II ∈ Conn
116 115 a1i ⊢ ( 𝜑 → II ∈ Conn )
117 iinllyconn ⊢ II ∈ 𝑛-Locally Conn
118 117 a1i ⊢ ( 𝜑 → II ∈ 𝑛-Locally Conn )
119 38 63 61 10 cnmpt12f ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) ∈ ( II Cn 𝐶 ) )
120 cvmtop1 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
121 4 120 syl ⊢ ( 𝜑 → 𝐶 ∈ Top )
122 1 toptopon ⊢ ( 𝐶 ∈ Top ↔ 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
123 121 122 sylib ⊢ ( 𝜑 → 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
124 ffvelrn ⊢ ( ( 𝑀 : ( 0 [,] 1 ) ⟶ 𝐵 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑀 ‘ 0 ) ∈ 𝐵 )
125 83 25 124 sylancl ⊢ ( 𝜑 → ( 𝑀 ‘ 0 ) ∈ 𝐵 )
126 cnconst2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝐶 ∈ ( TopOn ‘ 𝐵 ) ∧ ( 𝑀 ‘ 0 ) ∈ 𝐵 ) → ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 0 ) } ) ∈ ( II Cn 𝐶 ) )
127 38 123 125 126 syl3anc ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 0 ) } ) ∈ ( II Cn 𝐶 ) )
128 7 8 9 phtpyi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝐾 𝑠 ) = ( 𝐺 ‘ 0 ) ∧ ( 1 𝐾 𝑠 ) = ( 𝐺 ‘ 1 ) ) )
129 128 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐾 𝑠 ) = ( 𝐺 ‘ 0 ) )
130 opelxpi ⊢ ( ( 0 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ⟨ 0 , 𝑠 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
131 25 130 mpan ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ⟨ 0 , 𝑠 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
132 fvco3 ⊢ ( ( 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ ⟨ 0 , 𝑠 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( ( 𝐹 ∘ 𝐴 ) ‘ ⟨ 0 , 𝑠 ⟩ ) = ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 0 , 𝑠 ⟩ ) ) )
133 24 131 132 syl2an ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝐴 ) ‘ ⟨ 0 , 𝑠 ⟩ ) = ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 0 , 𝑠 ⟩ ) ) )
134 30 fveq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝐴 ) ‘ ⟨ 0 , 𝑠 ⟩ ) = ( 𝐾 ‘ ⟨ 0 , 𝑠 ⟩ ) )
135 133 134 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 0 , 𝑠 ⟩ ) ) = ( 𝐾 ‘ ⟨ 0 , 𝑠 ⟩ ) )
136 df-ov ⊢ ( 0 𝐴 𝑠 ) = ( 𝐴 ‘ ⟨ 0 , 𝑠 ⟩ )
137 136 fveq2i ⊢ ( 𝐹 ‘ ( 0 𝐴 𝑠 ) ) = ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 0 , 𝑠 ⟩ ) )
138 df-ov ⊢ ( 0 𝐾 𝑠 ) = ( 𝐾 ‘ ⟨ 0 , 𝑠 ⟩ )
139 135 137 138 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 0 𝐴 𝑠 ) ) = ( 0 𝐾 𝑠 ) )
140 13 simp3d ⊢ ( 𝜑 → ( 𝑀 ‘ 0 ) = 𝑃 )
141 140 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑀 ‘ 0 ) = 𝑃 )
142 141 fveq2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝑀 ‘ 0 ) ) = ( 𝐹 ‘ 𝑃 ) )
143 6 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
144 142 143 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝑀 ‘ 0 ) ) = ( 𝐺 ‘ 0 ) )
145 129 139 144 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 0 𝐴 𝑠 ) ) = ( 𝐹 ‘ ( 𝑀 ‘ 0 ) ) )
146 145 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 0 𝐴 𝑠 ) ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 𝑀 ‘ 0 ) ) ) )
147 fconstmpt ⊢ ( ( 0 [,] 1 ) × { ( 𝐹 ‘ ( 𝑀 ‘ 0 ) ) } ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 𝑀 ‘ 0 ) ) )
148 146 147 eqtr4di ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 0 𝐴 𝑠 ) ) ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ ( 𝑀 ‘ 0 ) ) } ) )
149 fovrn ⊢ ( ( 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ 0 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐴 𝑠 ) ∈ 𝐵 )
150 25 149 mp3an2 ⊢ ( ( 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐴 𝑠 ) ∈ 𝐵 )
151 24 150 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐴 𝑠 ) ∈ 𝐵 )
152 eqidd ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) )
153 fveq2 ⊢ ( 𝑥 = ( 0 𝐴 𝑠 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 0 𝐴 𝑠 ) ) )
154 151 152 54 153 fmptco ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 0 𝐴 𝑠 ) ) ) )
155 53 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
156 fcoconst ⊢ ( ( 𝐹 Fn 𝐵 ∧ ( 𝑀 ‘ 0 ) ∈ 𝐵 ) → ( 𝐹 ∘ ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 0 ) } ) ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ ( 𝑀 ‘ 0 ) ) } ) )
157 155 125 156 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 0 ) } ) ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ ( 𝑀 ‘ 0 ) ) } ) )
158 148 154 157 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) ) = ( 𝐹 ∘ ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 0 ) } ) ) )
159 12 140 eqtr4d ⊢ ( 𝜑 → ( 0 𝐴 0 ) = ( 𝑀 ‘ 0 ) )
160 oveq2 ⊢ ( 𝑠 = 0 → ( 0 𝐴 𝑠 ) = ( 0 𝐴 0 ) )
161 eqid ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) )
162 160 161 72 fvmpt ⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) ‘ 0 ) = ( 0 𝐴 0 ) )
163 25 162 ax-mp ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) ‘ 0 ) = ( 0 𝐴 0 )
164 fvex ⊢ ( 𝑀 ‘ 0 ) ∈ V
165 164 fvconst2 ⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 0 ) } ) ‘ 0 ) = ( 𝑀 ‘ 0 ) )
166 25 165 ax-mp ⊢ ( ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 0 ) } ) ‘ 0 ) = ( 𝑀 ‘ 0 )
167 159 163 166 3eqtr4g ⊢ ( 𝜑 → ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) ‘ 0 ) = ( ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 0 ) } ) ‘ 0 ) )
168 1 21 4 116 118 62 119 127 158 167 cvmliftmoi ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) = ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 0 ) } ) )
169 fconstmpt ⊢ ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 0 ) } ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑀 ‘ 0 ) )
170 168 169 eqtrdi ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑀 ‘ 0 ) ) )
171 mpteqb ⊢ ( ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 0 𝐴 𝑠 ) ∈ V → ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑀 ‘ 0 ) ) ↔ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 0 𝐴 𝑠 ) = ( 𝑀 ‘ 0 ) ) )
172 ovexd ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ( 0 𝐴 𝑠 ) ∈ V )
173 171 172 mprg ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 0 𝐴 𝑠 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑀 ‘ 0 ) ) ↔ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 0 𝐴 𝑠 ) = ( 𝑀 ‘ 0 ) )
174 170 173 sylib ⊢ ( 𝜑 → ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 0 𝐴 𝑠 ) = ( 𝑀 ‘ 0 ) )
175 oveq2 ⊢ ( 𝑠 = 1 → ( 0 𝐴 𝑠 ) = ( 0 𝐴 1 ) )
176 175 eqeq1d ⊢ ( 𝑠 = 1 → ( ( 0 𝐴 𝑠 ) = ( 𝑀 ‘ 0 ) ↔ ( 0 𝐴 1 ) = ( 𝑀 ‘ 0 ) ) )
177 176 rspcv ⊢ ( 1 ∈ ( 0 [,] 1 ) → ( ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 0 𝐴 𝑠 ) = ( 𝑀 ‘ 0 ) → ( 0 𝐴 1 ) = ( 𝑀 ‘ 0 ) ) )
178 91 174 177 mpsyl ⊢ ( 𝜑 → ( 0 𝐴 1 ) = ( 𝑀 ‘ 0 ) )
179 178 140 eqtrd ⊢ ( 𝜑 → ( 0 𝐴 1 ) = 𝑃 )
180 91 a1i ⊢ ( 𝜑 → 1 ∈ ( 0 [,] 1 ) )
181 38 38 180 cnmptc ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ 1 ) ∈ ( II Cn II ) )
182 38 61 181 10 cnmpt12f ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ∈ ( II Cn 𝐶 ) )
183 1 cvmlift ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐻 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( 𝐻 ‘ 0 ) ) ) → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐻 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
184 4 8 5 17 183 syl22anc ⊢ ( 𝜑 → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐻 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
185 coeq2 ⊢ ( 𝑓 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) → ( 𝐹 ∘ 𝑓 ) = ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ) )
186 185 eqeq1d ⊢ ( 𝑓 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) → ( ( 𝐹 ∘ 𝑓 ) = 𝐻 ↔ ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ) = 𝐻 ) )
187 fveq1 ⊢ ( 𝑓 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) → ( 𝑓 ‘ 0 ) = ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ‘ 0 ) )
188 oveq1 ⊢ ( 𝑠 = 0 → ( 𝑠 𝐴 1 ) = ( 0 𝐴 1 ) )
189 eqid ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) )
190 ovex ⊢ ( 0 𝐴 1 ) ∈ V
191 188 189 190 fvmpt ⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ‘ 0 ) = ( 0 𝐴 1 ) )
192 25 191 ax-mp ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ‘ 0 ) = ( 0 𝐴 1 )
193 187 192 eqtrdi ⊢ ( 𝑓 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) → ( 𝑓 ‘ 0 ) = ( 0 𝐴 1 ) )
194 193 eqeq1d ⊢ ( 𝑓 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) → ( ( 𝑓 ‘ 0 ) = 𝑃 ↔ ( 0 𝐴 1 ) = 𝑃 ) )
195 186 194 anbi12d ⊢ ( 𝑓 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) → ( ( ( 𝐹 ∘ 𝑓 ) = 𝐻 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ) = 𝐻 ∧ ( 0 𝐴 1 ) = 𝑃 ) ) )
196 195 riota2 ⊢ ( ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ∈ ( II Cn 𝐶 ) ∧ ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐻 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) → ( ( ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ) = 𝐻 ∧ ( 0 𝐴 1 ) = 𝑃 ) ↔ ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐻 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ) )
197 182 184 196 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ) = 𝐻 ∧ ( 0 𝐴 1 ) = 𝑃 ) ↔ ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐻 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) ) )
198 114 179 197 mpbi2and ⊢ ( 𝜑 → ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐻 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) )
199 3 198 syl5eq ⊢ ( 𝜑 → 𝑁 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) )
200 21 1 cnf ⊢ ( 𝑁 ∈ ( II Cn 𝐶 ) → 𝑁 : ( 0 [,] 1 ) ⟶ 𝐵 )
201 19 200 syl ⊢ ( 𝜑 → 𝑁 : ( 0 [,] 1 ) ⟶ 𝐵 )
202 201 feqmptd ⊢ ( 𝜑 → 𝑁 = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑁 ‘ 𝑠 ) ) )
203 199 202 eqtr3d ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑁 ‘ 𝑠 ) ) )
204 mpteqb ⊢ ( ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 𝑠 𝐴 1 ) ∈ V → ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑁 ‘ 𝑠 ) ) ↔ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 𝑠 𝐴 1 ) = ( 𝑁 ‘ 𝑠 ) ) )
205 ovexd ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ( 𝑠 𝐴 1 ) ∈ V )
206 204 205 mprg ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑠 𝐴 1 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑁 ‘ 𝑠 ) ) ↔ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 𝑠 𝐴 1 ) = ( 𝑁 ‘ 𝑠 ) )
207 203 206 sylib ⊢ ( 𝜑 → ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 𝑠 𝐴 1 ) = ( 𝑁 ‘ 𝑠 ) )
208 207 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 𝐴 1 ) = ( 𝑁 ‘ 𝑠 ) )
209 174 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 𝐴 𝑠 ) = ( 𝑀 ‘ 0 ) )
210 38 181 61 10 cnmpt12f ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) ∈ ( II Cn 𝐶 ) )
211 ffvelrn ⊢ ( ( 𝑀 : ( 0 [,] 1 ) ⟶ 𝐵 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝑀 ‘ 1 ) ∈ 𝐵 )
212 83 91 211 sylancl ⊢ ( 𝜑 → ( 𝑀 ‘ 1 ) ∈ 𝐵 )
213 cnconst2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝐶 ∈ ( TopOn ‘ 𝐵 ) ∧ ( 𝑀 ‘ 1 ) ∈ 𝐵 ) → ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 1 ) } ) ∈ ( II Cn 𝐶 ) )
214 38 123 212 213 syl3anc ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 1 ) } ) ∈ ( II Cn 𝐶 ) )
215 opelxpi ⊢ ( ( 1 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ⟨ 1 , 𝑠 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
216 91 215 mpan ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ⟨ 1 , 𝑠 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
217 fvco3 ⊢ ( ( 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ ⟨ 1 , 𝑠 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ) → ( ( 𝐹 ∘ 𝐴 ) ‘ ⟨ 1 , 𝑠 ⟩ ) = ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 1 , 𝑠 ⟩ ) ) )
218 24 216 217 syl2an ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝐴 ) ‘ ⟨ 1 , 𝑠 ⟩ ) = ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 1 , 𝑠 ⟩ ) ) )
219 30 fveq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝐴 ) ‘ ⟨ 1 , 𝑠 ⟩ ) = ( 𝐾 ‘ ⟨ 1 , 𝑠 ⟩ ) )
220 218 219 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 1 , 𝑠 ⟩ ) ) = ( 𝐾 ‘ ⟨ 1 , 𝑠 ⟩ ) )
221 df-ov ⊢ ( 1 𝐴 𝑠 ) = ( 𝐴 ‘ ⟨ 1 , 𝑠 ⟩ )
222 221 fveq2i ⊢ ( 𝐹 ‘ ( 1 𝐴 𝑠 ) ) = ( 𝐹 ‘ ( 𝐴 ‘ ⟨ 1 , 𝑠 ⟩ ) )
223 df-ov ⊢ ( 1 𝐾 𝑠 ) = ( 𝐾 ‘ ⟨ 1 , 𝑠 ⟩ )
224 220 222 223 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 1 𝐴 𝑠 ) ) = ( 1 𝐾 𝑠 ) )
225 128 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐾 𝑠 ) = ( 𝐺 ‘ 1 ) )
226 13 simp2d ⊢ ( 𝜑 → ( 𝐹 ∘ 𝑀 ) = 𝐺 )
227 226 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ∘ 𝑀 ) = 𝐺 )
228 227 fveq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝑀 ) ‘ 1 ) = ( 𝐺 ‘ 1 ) )
229 83 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → 𝑀 : ( 0 [,] 1 ) ⟶ 𝐵 )
230 fvco3 ⊢ ( ( 𝑀 : ( 0 [,] 1 ) ⟶ 𝐵 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝑀 ) ‘ 1 ) = ( 𝐹 ‘ ( 𝑀 ‘ 1 ) ) )
231 229 91 230 sylancl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝑀 ) ‘ 1 ) = ( 𝐹 ‘ ( 𝑀 ‘ 1 ) ) )
232 228 231 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐺 ‘ 1 ) = ( 𝐹 ‘ ( 𝑀 ‘ 1 ) ) )
233 224 225 232 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 1 𝐴 𝑠 ) ) = ( 𝐹 ‘ ( 𝑀 ‘ 1 ) ) )
234 233 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 𝐴 𝑠 ) ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 𝑀 ‘ 1 ) ) ) )
235 fconstmpt ⊢ ( ( 0 [,] 1 ) × { ( 𝐹 ‘ ( 𝑀 ‘ 1 ) ) } ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 𝑀 ‘ 1 ) ) )
236 234 235 eqtr4di ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 𝐴 𝑠 ) ) ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ ( 𝑀 ‘ 1 ) ) } ) )
237 fovrn ⊢ ( ( 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ 1 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐴 𝑠 ) ∈ 𝐵 )
238 91 237 mp3an2 ⊢ ( ( 𝐴 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐴 𝑠 ) ∈ 𝐵 )
239 24 238 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐴 𝑠 ) ∈ 𝐵 )
240 eqidd ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) )
241 fveq2 ⊢ ( 𝑥 = ( 1 𝐴 𝑠 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 1 𝐴 𝑠 ) ) )
242 239 240 54 241 fmptco ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝐹 ‘ ( 1 𝐴 𝑠 ) ) ) )
243 fcoconst ⊢ ( ( 𝐹 Fn 𝐵 ∧ ( 𝑀 ‘ 1 ) ∈ 𝐵 ) → ( 𝐹 ∘ ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 1 ) } ) ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ ( 𝑀 ‘ 1 ) ) } ) )
244 155 212 243 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 1 ) } ) ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ ( 𝑀 ‘ 1 ) ) } ) )
245 236 242 244 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) ) = ( 𝐹 ∘ ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 1 ) } ) ) )
246 oveq1 ⊢ ( 𝑠 = 1 → ( 𝑠 𝐴 0 ) = ( 1 𝐴 0 ) )
247 fveq2 ⊢ ( 𝑠 = 1 → ( 𝑀 ‘ 𝑠 ) = ( 𝑀 ‘ 1 ) )
248 246 247 eqeq12d ⊢ ( 𝑠 = 1 → ( ( 𝑠 𝐴 0 ) = ( 𝑀 ‘ 𝑠 ) ↔ ( 1 𝐴 0 ) = ( 𝑀 ‘ 1 ) ) )
249 248 rspcv ⊢ ( 1 ∈ ( 0 [,] 1 ) → ( ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 𝑠 𝐴 0 ) = ( 𝑀 ‘ 𝑠 ) → ( 1 𝐴 0 ) = ( 𝑀 ‘ 1 ) ) )
250 91 89 249 mpsyl ⊢ ( 𝜑 → ( 1 𝐴 0 ) = ( 𝑀 ‘ 1 ) )
251 oveq2 ⊢ ( 𝑠 = 0 → ( 1 𝐴 𝑠 ) = ( 1 𝐴 0 ) )
252 eqid ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) )
253 ovex ⊢ ( 1 𝐴 0 ) ∈ V
254 251 252 253 fvmpt ⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) ‘ 0 ) = ( 1 𝐴 0 ) )
255 25 254 ax-mp ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) ‘ 0 ) = ( 1 𝐴 0 )
256 fvex ⊢ ( 𝑀 ‘ 1 ) ∈ V
257 256 fvconst2 ⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 1 ) } ) ‘ 0 ) = ( 𝑀 ‘ 1 ) )
258 25 257 ax-mp ⊢ ( ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 1 ) } ) ‘ 0 ) = ( 𝑀 ‘ 1 )
259 250 255 258 3eqtr4g ⊢ ( 𝜑 → ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) ‘ 0 ) = ( ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 1 ) } ) ‘ 0 ) )
260 1 21 4 116 118 62 210 214 245 259 cvmliftmoi ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) = ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 1 ) } ) )
261 fconstmpt ⊢ ( ( 0 [,] 1 ) × { ( 𝑀 ‘ 1 ) } ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑀 ‘ 1 ) )
262 260 261 eqtrdi ⊢ ( 𝜑 → ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑀 ‘ 1 ) ) )
263 mpteqb ⊢ ( ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 1 𝐴 𝑠 ) ∈ V → ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑀 ‘ 1 ) ) ↔ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 1 𝐴 𝑠 ) = ( 𝑀 ‘ 1 ) ) )
264 ovexd ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ( 1 𝐴 𝑠 ) ∈ V )
265 263 264 mprg ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 1 𝐴 𝑠 ) ) = ( 𝑠 ∈ ( 0 [,] 1 ) ↦ ( 𝑀 ‘ 1 ) ) ↔ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 1 𝐴 𝑠 ) = ( 𝑀 ‘ 1 ) )
266 262 265 sylib ⊢ ( 𝜑 → ∀ 𝑠 ∈ ( 0 [,] 1 ) ( 1 𝐴 𝑠 ) = ( 𝑀 ‘ 1 ) )
267 266 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 𝐴 𝑠 ) = ( 𝑀 ‘ 1 ) )
268 14 19 10 90 208 209 267 isphtpy2d ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑀 ( PHtpy ‘ 𝐶 ) 𝑁 ) )