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 ‘ 𝐶 ) 𝑁 ) )