Metamath Proof Explorer

Theorem cvmlift2lem13

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses cvmlift2.b ⊢ 𝐵 = ∪ 𝐶
cvmlift2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmlift2.g ⊢ ( 𝜑 → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
cvmlift2.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmlift2.i ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 0 𝐺 0 ) )
cvmlift2.h ⊢ 𝐻 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
cvmlift2.k ⊢ 𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑥 ) ) ) ‘ 𝑦 ) )
Assertion cvmlift2lem13 ( 𝜑 → ∃! 𝑔 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 0 𝑔 0 ) = 𝑃 ) )

Proof

Step Hyp Ref Expression
1 cvmlift2.b ⊢ 𝐵 = ∪ 𝐶
2 cvmlift2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
3 cvmlift2.g ⊢ ( 𝜑 → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
4 cvmlift2.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
5 cvmlift2.i ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 0 𝐺 0 ) )
6 cvmlift2.h ⊢ 𝐻 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
7 cvmlift2.k ⊢ 𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑥 ) ) ) ‘ 𝑦 ) )
8 fveq2 ⊢ ( 𝑎 = 𝑧 → ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) = ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) )
9 8 eleq2d ⊢ ( 𝑎 = 𝑧 → ( 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) ↔ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) ) )
10 9 cbvrabv ⊢ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } = { 𝑧 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑧 ) }
11 sneq ⊢ ( 𝑧 = 𝑏 → { 𝑧 } = { 𝑏 } )
12 11 xpeq2d ⊢ ( 𝑧 = 𝑏 → ( ( 0 [,] 1 ) × { 𝑧 } ) = ( ( 0 [,] 1 ) × { 𝑏 } ) )
13 12 sseq1d ⊢ ( 𝑧 = 𝑏 → ( ( ( 0 [,] 1 ) × { 𝑧 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( ( 0 [,] 1 ) × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) )
14 13 cbvrabv ⊢ { 𝑧 ∈ ( 0 [,] 1 ) ∣ ( ( 0 [,] 1 ) × { 𝑧 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } } = { 𝑏 ∈ ( 0 [,] 1 ) ∣ ( ( 0 [,] 1 ) × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } }
15 simpr ⊢ ( ( 𝑐 = 𝑟 ∧ 𝑑 = 𝑡 ) → 𝑑 = 𝑡 )
16 15 eleq1d ⊢ ( ( 𝑐 = 𝑟 ∧ 𝑑 = 𝑡 ) → ( 𝑑 ∈ ( 0 [,] 1 ) ↔ 𝑡 ∈ ( 0 [,] 1 ) ) )
17 xpeq1 ⊢ ( 𝑣 = 𝑢 → ( 𝑣 × { 𝑏 } ) = ( 𝑢 × { 𝑏 } ) )
18 17 sseq1d ⊢ ( 𝑣 = 𝑢 → ( ( 𝑣 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑢 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) )
19 xpeq1 ⊢ ( 𝑣 = 𝑢 → ( 𝑣 × { 𝑑 } ) = ( 𝑢 × { 𝑑 } ) )
20 19 sseq1d ⊢ ( 𝑣 = 𝑢 → ( ( 𝑣 × { 𝑑 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑢 × { 𝑑 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) )
21 18 20 bibi12d ⊢ ( 𝑣 = 𝑢 → ( ( ( 𝑣 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑣 × { 𝑑 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ↔ ( ( 𝑢 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑢 × { 𝑑 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ) )
22 21 cbvrexvw ⊢ ( ∃ 𝑣 ∈ ( ( nei ‘ II ) ‘ { 𝑐 } ) ( ( 𝑣 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑣 × { 𝑑 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ↔ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑐 } ) ( ( 𝑢 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑢 × { 𝑑 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) )
23 simpl ⊢ ( ( 𝑐 = 𝑟 ∧ 𝑑 = 𝑡 ) → 𝑐 = 𝑟 )
24 23 sneqd ⊢ ( ( 𝑐 = 𝑟 ∧ 𝑑 = 𝑡 ) → { 𝑐 } = { 𝑟 } )
25 24 fveq2d ⊢ ( ( 𝑐 = 𝑟 ∧ 𝑑 = 𝑡 ) → ( ( nei ‘ II ) ‘ { 𝑐 } ) = ( ( nei ‘ II ) ‘ { 𝑟 } ) )
26 15 sneqd ⊢ ( ( 𝑐 = 𝑟 ∧ 𝑑 = 𝑡 ) → { 𝑑 } = { 𝑡 } )
27 26 xpeq2d ⊢ ( ( 𝑐 = 𝑟 ∧ 𝑑 = 𝑡 ) → ( 𝑢 × { 𝑑 } ) = ( 𝑢 × { 𝑡 } ) )
28 27 sseq1d ⊢ ( ( 𝑐 = 𝑟 ∧ 𝑑 = 𝑡 ) → ( ( 𝑢 × { 𝑑 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑢 × { 𝑡 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) )
29 28 bibi2d ⊢ ( ( 𝑐 = 𝑟 ∧ 𝑑 = 𝑡 ) → ( ( ( 𝑢 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑢 × { 𝑑 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ↔ ( ( 𝑢 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑢 × { 𝑡 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ) )
30 25 29 rexeqbidv ⊢ ( ( 𝑐 = 𝑟 ∧ 𝑑 = 𝑡 ) → ( ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑐 } ) ( ( 𝑢 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑢 × { 𝑑 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ↔ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑢 × { 𝑡 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ) )
31 22 30 syl5bb ⊢ ( ( 𝑐 = 𝑟 ∧ 𝑑 = 𝑡 ) → ( ∃ 𝑣 ∈ ( ( nei ‘ II ) ‘ { 𝑐 } ) ( ( 𝑣 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑣 × { 𝑑 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ↔ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑢 × { 𝑡 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ) )
32 16 31 anbi12d ⊢ ( ( 𝑐 = 𝑟 ∧ 𝑑 = 𝑡 ) → ( ( 𝑑 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑣 ∈ ( ( nei ‘ II ) ‘ { 𝑐 } ) ( ( 𝑣 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑣 × { 𝑑 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ) ↔ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑢 × { 𝑡 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ) ) )
33 32 cbvopabv ⊢ { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( 𝑑 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑣 ∈ ( ( nei ‘ II ) ‘ { 𝑐 } ) ( ( 𝑣 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑣 × { 𝑑 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ) } = { ⟨ 𝑟 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∃ 𝑢 ∈ ( ( nei ‘ II ) ‘ { 𝑟 } ) ( ( 𝑢 × { 𝑏 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ↔ ( 𝑢 × { 𝑡 } ) ⊆ { 𝑎 ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ∣ 𝐾 ∈ ( ( ( II ×t II ) CnP 𝐶 ) ‘ 𝑎 ) } ) ) }
34 1 2 3 4 5 6 7 10 14 33 cvmlift2lem12 ⊢ ( 𝜑 → 𝐾 ∈ ( ( II ×t II ) Cn 𝐶 ) )
35 1 2 3 4 5 6 7 cvmlift2lem7 ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐾 ) = 𝐺 )
36 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
37 1 2 3 4 5 6 7 cvmlift2lem8 ⊢ ( ( 𝜑 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 0 𝐾 0 ) = ( 𝐻 ‘ 0 ) )
38 36 37 mpan2 ⊢ ( 𝜑 → ( 0 𝐾 0 ) = ( 𝐻 ‘ 0 ) )
39 1 2 3 4 5 6 cvmlift2lem2 ⊢ ( 𝜑 → ( 𝐻 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐻 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝐻 ‘ 0 ) = 𝑃 ) )
40 39 simp3d ⊢ ( 𝜑 → ( 𝐻 ‘ 0 ) = 𝑃 )
41 38 40 eqtrd ⊢ ( 𝜑 → ( 0 𝐾 0 ) = 𝑃 )
42 coeq2 ⊢ ( 𝑔 = 𝐾 → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ 𝐾 ) )
43 42 eqeq1d ⊢ ( 𝑔 = 𝐾 → ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ↔ ( 𝐹 ∘ 𝐾 ) = 𝐺 ) )
44 oveq ⊢ ( 𝑔 = 𝐾 → ( 0 𝑔 0 ) = ( 0 𝐾 0 ) )
45 44 eqeq1d ⊢ ( 𝑔 = 𝐾 → ( ( 0 𝑔 0 ) = 𝑃 ↔ ( 0 𝐾 0 ) = 𝑃 ) )
46 43 45 anbi12d ⊢ ( 𝑔 = 𝐾 → ( ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 0 𝑔 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝐾 ) = 𝐺 ∧ ( 0 𝐾 0 ) = 𝑃 ) ) )
47 46 rspcev ⊢ ( ( 𝐾 ∈ ( ( II ×t II ) Cn 𝐶 ) ∧ ( ( 𝐹 ∘ 𝐾 ) = 𝐺 ∧ ( 0 𝐾 0 ) = 𝑃 ) ) → ∃ 𝑔 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 0 𝑔 0 ) = 𝑃 ) )
48 34 35 41 47 syl12anc ⊢ ( 𝜑 → ∃ 𝑔 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 0 𝑔 0 ) = 𝑃 ) )
49 iitop ⊢ II ∈ Top
50 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
51 49 49 50 50 txunii ⊢ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) = ∪ ( II ×t II )
52 iiconn ⊢ II ∈ Conn
53 txconn ⊢ ( ( II ∈ Conn ∧ II ∈ Conn ) → ( II ×t II ) ∈ Conn )
54 52 52 53 mp2an ⊢ ( II ×t II ) ∈ Conn
55 54 a1i ⊢ ( 𝜑 → ( II ×t II ) ∈ Conn )
56 iinllyconn ⊢ II ∈ 𝑛-Locally Conn
57 txconn ⊢ ( ( 𝑥 ∈ Conn ∧ 𝑦 ∈ Conn ) → ( 𝑥 ×t 𝑦 ) ∈ Conn )
58 57 txnlly ⊢ ( ( II ∈ 𝑛-Locally Conn ∧ II ∈ 𝑛-Locally Conn ) → ( II ×t II ) ∈ 𝑛-Locally Conn )
59 56 56 58 mp2an ⊢ ( II ×t II ) ∈ 𝑛-Locally Conn
60 59 a1i ⊢ ( 𝜑 → ( II ×t II ) ∈ 𝑛-Locally Conn )
61 opelxpi ⊢ ( ( 0 ∈ ( 0 [,] 1 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ⟨ 0 , 0 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
62 36 36 61 mp2an ⊢ ⟨ 0 , 0 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) )
63 62 a1i ⊢ ( 𝜑 → ⟨ 0 , 0 ⟩ ∈ ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
64 df-ov ⊢ ( 0 𝐺 0 ) = ( 𝐺 ‘ ⟨ 0 , 0 ⟩ )
65 5 64 eqtrdi ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ ⟨ 0 , 0 ⟩ ) )
66 1 51 2 55 60 63 3 4 65 cvmliftmo ⊢ ( 𝜑 → ∃* 𝑔 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ ⟨ 0 , 0 ⟩ ) = 𝑃 ) )
67 df-ov ⊢ ( 0 𝑔 0 ) = ( 𝑔 ‘ ⟨ 0 , 0 ⟩ )
68 67 eqeq1i ⊢ ( ( 0 𝑔 0 ) = 𝑃 ↔ ( 𝑔 ‘ ⟨ 0 , 0 ⟩ ) = 𝑃 )
69 68 anbi2i ⊢ ( ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 0 𝑔 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ ⟨ 0 , 0 ⟩ ) = 𝑃 ) )
70 69 rmobii ⊢ ( ∃* 𝑔 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 0 𝑔 0 ) = 𝑃 ) ↔ ∃* 𝑔 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ ⟨ 0 , 0 ⟩ ) = 𝑃 ) )
71 66 70 sylibr ⊢ ( 𝜑 → ∃* 𝑔 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 0 𝑔 0 ) = 𝑃 ) )
72 reu5 ⊢ ( ∃! 𝑔 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 0 𝑔 0 ) = 𝑃 ) ↔ ( ∃ 𝑔 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 0 𝑔 0 ) = 𝑃 ) ∧ ∃* 𝑔 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 0 𝑔 0 ) = 𝑃 ) ) )
73 48 71 72 sylanbrc ⊢ ( 𝜑 → ∃! 𝑔 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 0 𝑔 0 ) = 𝑃 ) )