Metamath Proof Explorer

Theorem cvmlift3lem6

Description: Lemma for cvmlift3 . (Contributed by Mario Carneiro, 9-Jul-2015)

Ref Expression
Hypotheses cvmlift3.b ⊢ 𝐵 = ∪ 𝐶
cvmlift3.y ⊢ 𝑌 = ∪ 𝐾
cvmlift3.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmlift3.k ⊢ ( 𝜑 → 𝐾 ∈ SConn )
cvmlift3.l ⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally PConn )
cvmlift3.o ⊢ ( 𝜑 → 𝑂 ∈ 𝑌 )
cvmlift3.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
cvmlift3.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmlift3.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
cvmlift3.h ⊢ 𝐻 = ( 𝑥 ∈ 𝑌 ↦ ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
cvmlift3lem7.s ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
cvmlift3lem7.1 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ 𝐴 )
cvmlift3lem7.2 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) )
cvmlift3lem7.3 ⊢ ( 𝜑 → 𝑀 ⊆ ( ◡ 𝐺 “ 𝐴 ) )
cvmlift3lem7.w ⊢ 𝑊 = ( ℩ 𝑏 ∈ 𝑇 ( 𝐻 ‘ 𝑋 ) ∈ 𝑏 )
cvmlift3lem6.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑀 )
cvmlift3lem6.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑀 )
cvmlift3lem6.q ⊢ ( 𝜑 → 𝑄 ∈ ( II Cn 𝐾 ) )
cvmlift3lem6.r ⊢ 𝑅 = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑄 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
cvmlift3lem6.1 ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝑂 ∧ ( 𝑄 ‘ 1 ) = 𝑋 ∧ ( 𝑅 ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) )
cvmlift3lem6.n ⊢ ( 𝜑 → 𝑁 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) )
cvmlift3lem6.2 ⊢ ( 𝜑 → ( ( 𝑁 ‘ 0 ) = 𝑋 ∧ ( 𝑁 ‘ 1 ) = 𝑍 ) )
cvmlift3lem6.i ⊢ 𝐼 = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝑔 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )
Assertion cvmlift3lem6 ( 𝜑 → ( 𝐻 ‘ 𝑍 ) ∈ 𝑊 )

Proof

Step Hyp Ref Expression
1 cvmlift3.b ⊢ 𝐵 = ∪ 𝐶
2 cvmlift3.y ⊢ 𝑌 = ∪ 𝐾
3 cvmlift3.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
4 cvmlift3.k ⊢ ( 𝜑 → 𝐾 ∈ SConn )
5 cvmlift3.l ⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally PConn )
6 cvmlift3.o ⊢ ( 𝜑 → 𝑂 ∈ 𝑌 )
7 cvmlift3.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
8 cvmlift3.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
9 cvmlift3.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
10 cvmlift3.h ⊢ 𝐻 = ( 𝑥 ∈ 𝑌 ↦ ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
11 cvmlift3lem7.s ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
12 cvmlift3lem7.1 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ 𝐴 )
13 cvmlift3lem7.2 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) )
14 cvmlift3lem7.3 ⊢ ( 𝜑 → 𝑀 ⊆ ( ◡ 𝐺 “ 𝐴 ) )
15 cvmlift3lem7.w ⊢ 𝑊 = ( ℩ 𝑏 ∈ 𝑇 ( 𝐻 ‘ 𝑋 ) ∈ 𝑏 )
16 cvmlift3lem6.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑀 )
17 cvmlift3lem6.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑀 )
18 cvmlift3lem6.q ⊢ ( 𝜑 → 𝑄 ∈ ( II Cn 𝐾 ) )
19 cvmlift3lem6.r ⊢ 𝑅 = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑄 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
20 cvmlift3lem6.1 ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝑂 ∧ ( 𝑄 ‘ 1 ) = 𝑋 ∧ ( 𝑅 ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) )
21 cvmlift3lem6.n ⊢ ( 𝜑 → 𝑁 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) )
22 cvmlift3lem6.2 ⊢ ( 𝜑 → ( ( 𝑁 ‘ 0 ) = 𝑋 ∧ ( 𝑁 ‘ 1 ) = 𝑍 ) )
23 cvmlift3lem6.i ⊢ 𝐼 = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝑔 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )
24 sconntop ⊢ ( 𝐾 ∈ SConn → 𝐾 ∈ Top )
25 4 24 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
26 cnrest2r ⊢ ( 𝐾 ∈ Top → ( II Cn ( 𝐾 ↾t 𝑀 ) ) ⊆ ( II Cn 𝐾 ) )
27 25 26 syl ⊢ ( 𝜑 → ( II Cn ( 𝐾 ↾t 𝑀 ) ) ⊆ ( II Cn 𝐾 ) )
28 27 21 sseldd ⊢ ( 𝜑 → 𝑁 ∈ ( II Cn 𝐾 ) )
29 20 simp2d ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) = 𝑋 )
30 22 simpld ⊢ ( 𝜑 → ( 𝑁 ‘ 0 ) = 𝑋 )
31 29 30 eqtr4d ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) = ( 𝑁 ‘ 0 ) )
32 18 28 31 pcocn ⊢ ( 𝜑 → ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ∈ ( II Cn 𝐾 ) )
33 18 28 pco0 ⊢ ( 𝜑 → ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 0 ) = ( 𝑄 ‘ 0 ) )
34 20 simp1d ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝑂 )
35 33 34 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 0 ) = 𝑂 )
36 18 28 pco1 ⊢ ( 𝜑 → ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 1 ) = ( 𝑁 ‘ 1 ) )
37 22 simprd ⊢ ( 𝜑 → ( 𝑁 ‘ 1 ) = 𝑍 )
38 36 37 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 1 ) = 𝑍 )
39 cnco ⊢ ( ( 𝑄 ∈ ( II Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝐺 ∘ 𝑄 ) ∈ ( II Cn 𝐽 ) )
40 18 7 39 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝑄 ) ∈ ( II Cn 𝐽 ) )
41 34 fveq2d ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑄 ‘ 0 ) ) = ( 𝐺 ‘ 𝑂 ) )
42 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
43 42 2 cnf ⊢ ( 𝑄 ∈ ( II Cn 𝐾 ) → 𝑄 : ( 0 [,] 1 ) ⟶ 𝑌 )
44 18 43 syl ⊢ ( 𝜑 → 𝑄 : ( 0 [,] 1 ) ⟶ 𝑌 )
45 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
46 fvco3 ⊢ ( ( 𝑄 : ( 0 [,] 1 ) ⟶ 𝑌 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 𝐺 ∘ 𝑄 ) ‘ 0 ) = ( 𝐺 ‘ ( 𝑄 ‘ 0 ) ) )
47 44 45 46 sylancl ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝑄 ) ‘ 0 ) = ( 𝐺 ‘ ( 𝑄 ‘ 0 ) ) )
48 41 47 9 3eqtr4rd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( ( 𝐺 ∘ 𝑄 ) ‘ 0 ) )
49 1 19 3 40 8 48 cvmliftiota ⊢ ( 𝜑 → ( 𝑅 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝑅 ) = ( 𝐺 ∘ 𝑄 ) ∧ ( 𝑅 ‘ 0 ) = 𝑃 ) )
50 49 simp2d ⊢ ( 𝜑 → ( 𝐹 ∘ 𝑅 ) = ( 𝐺 ∘ 𝑄 ) )
51 cnco ⊢ ( ( 𝑁 ∈ ( II Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝐺 ∘ 𝑁 ) ∈ ( II Cn 𝐽 ) )
52 28 7 51 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝑁 ) ∈ ( II Cn 𝐽 ) )
53 1 2 3 4 5 6 7 8 9 10 cvmlift3lem3 ⊢ ( 𝜑 → 𝐻 : 𝑌 ⟶ 𝐵 )
54 cnvimass ⊢ ( ◡ 𝐺 “ 𝐴 ) ⊆ dom 𝐺
55 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
56 2 55 cnf ⊢ ( 𝐺 ∈ ( 𝐾 Cn 𝐽 ) → 𝐺 : 𝑌 ⟶ ∪ 𝐽 )
57 7 56 syl ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ∪ 𝐽 )
58 54 57 fssdm ⊢ ( 𝜑 → ( ◡ 𝐺 “ 𝐴 ) ⊆ 𝑌 )
59 14 58 sstrd ⊢ ( 𝜑 → 𝑀 ⊆ 𝑌 )
60 59 16 sseldd ⊢ ( 𝜑 → 𝑋 ∈ 𝑌 )
61 53 60 ffvelcdmd ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) ∈ 𝐵 )
62 30 fveq2d ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑁 ‘ 0 ) ) = ( 𝐺 ‘ 𝑋 ) )
63 42 2 cnf ⊢ ( 𝑁 ∈ ( II Cn 𝐾 ) → 𝑁 : ( 0 [,] 1 ) ⟶ 𝑌 )
64 28 63 syl ⊢ ( 𝜑 → 𝑁 : ( 0 [,] 1 ) ⟶ 𝑌 )
65 fvco3 ⊢ ( ( 𝑁 : ( 0 [,] 1 ) ⟶ 𝑌 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 𝐺 ∘ 𝑁 ) ‘ 0 ) = ( 𝐺 ‘ ( 𝑁 ‘ 0 ) ) )
66 64 45 65 sylancl ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝑁 ) ‘ 0 ) = ( 𝐺 ‘ ( 𝑁 ‘ 0 ) ) )
67 fvco3 ⊢ ( ( 𝐻 : 𝑌 ⟶ 𝐵 ∧ 𝑋 ∈ 𝑌 ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) )
68 53 60 67 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) )
69 1 2 3 4 5 6 7 8 9 10 cvmlift3lem5 ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) = 𝐺 )
70 69 fveq1d ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
71 68 70 eqtr3d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) = ( 𝐺 ‘ 𝑋 ) )
72 62 66 71 3eqtr4rd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) = ( ( 𝐺 ∘ 𝑁 ) ‘ 0 ) )
73 1 23 3 52 61 72 cvmliftiota ⊢ ( 𝜑 → ( 𝐼 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐼 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝐼 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )
74 73 simp2d ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐼 ) = ( 𝐺 ∘ 𝑁 ) )
75 50 74 oveq12d ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝑅 ) ( *𝑝 ‘ 𝐽 ) ( 𝐹 ∘ 𝐼 ) ) = ( ( 𝐺 ∘ 𝑄 ) ( *𝑝 ‘ 𝐽 ) ( 𝐺 ∘ 𝑁 ) ) )
76 49 simp1d ⊢ ( 𝜑 → 𝑅 ∈ ( II Cn 𝐶 ) )
77 73 simp1d ⊢ ( 𝜑 → 𝐼 ∈ ( II Cn 𝐶 ) )
78 20 simp3d ⊢ ( 𝜑 → ( 𝑅 ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) )
79 73 simp3d ⊢ ( 𝜑 → ( 𝐼 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) )
80 78 79 eqtr4d ⊢ ( 𝜑 → ( 𝑅 ‘ 1 ) = ( 𝐼 ‘ 0 ) )
81 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
82 3 81 syl ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
83 76 77 80 82 copco ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ) = ( ( 𝐹 ∘ 𝑅 ) ( *𝑝 ‘ 𝐽 ) ( 𝐹 ∘ 𝐼 ) ) )
84 18 28 31 7 copco ⊢ ( 𝜑 → ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) = ( ( 𝐺 ∘ 𝑄 ) ( *𝑝 ‘ 𝐽 ) ( 𝐺 ∘ 𝑁 ) ) )
85 75 83 84 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) )
86 76 77 pco0 ⊢ ( 𝜑 → ( ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ‘ 0 ) = ( 𝑅 ‘ 0 ) )
87 49 simp3d ⊢ ( 𝜑 → ( 𝑅 ‘ 0 ) = 𝑃 )
88 86 87 eqtrd ⊢ ( 𝜑 → ( ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ‘ 0 ) = 𝑃 )
89 76 77 80 pcocn ⊢ ( 𝜑 → ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ∈ ( II Cn 𝐶 ) )
90 cnco ⊢ ( ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ∈ ( II Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∈ ( II Cn 𝐽 ) )
91 32 7 90 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∈ ( II Cn 𝐽 ) )
92 35 fveq2d ⊢ ( 𝜑 → ( 𝐺 ‘ ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 0 ) ) = ( 𝐺 ‘ 𝑂 ) )
93 42 2 cnf ⊢ ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ∈ ( II Cn 𝐾 ) → ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) : ( 0 [,] 1 ) ⟶ 𝑌 )
94 32 93 syl ⊢ ( 𝜑 → ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) : ( 0 [,] 1 ) ⟶ 𝑌 )
95 fvco3 ⊢ ( ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) : ( 0 [,] 1 ) ⟶ 𝑌 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ‘ 0 ) = ( 𝐺 ‘ ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 0 ) ) )
96 94 45 95 sylancl ⊢ ( 𝜑 → ( ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ‘ 0 ) = ( 𝐺 ‘ ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 0 ) ) )
97 92 96 9 3eqtr4rd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ‘ 0 ) )
98 1 cvmlift ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ‘ 0 ) ) ) → ∃! 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
99 3 91 8 97 98 syl22anc ⊢ ( 𝜑 → ∃! 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
100 coeq2 ⊢ ( 𝑔 = ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ) )
101 100 eqeq1d ⊢ ( 𝑔 = ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) → ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ↔ ( 𝐹 ∘ ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ) )
102 fveq1 ⊢ ( 𝑔 = ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) → ( 𝑔 ‘ 0 ) = ( ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ‘ 0 ) )
103 102 eqeq1d ⊢ ( 𝑔 = ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) → ( ( 𝑔 ‘ 0 ) = 𝑃 ↔ ( ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ‘ 0 ) = 𝑃 ) )
104 101 103 anbi12d ⊢ ( 𝑔 = ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) → ( ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ‘ 0 ) = 𝑃 ) ) )
105 104 riota2 ⊢ ( ( ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ∈ ( II Cn 𝐶 ) ∧ ∃! 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) → ( ( ( 𝐹 ∘ ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ‘ 0 ) = 𝑃 ) ↔ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ) )
106 89 99 105 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐹 ∘ ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ‘ 0 ) = 𝑃 ) ↔ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ) )
107 85 88 106 mpbi2and ⊢ ( 𝜑 → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) )
108 107 fveq1d ⊢ ( 𝜑 → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ‘ 1 ) )
109 76 77 pco1 ⊢ ( 𝜑 → ( ( 𝑅 ( *𝑝 ‘ 𝐶 ) 𝐼 ) ‘ 1 ) = ( 𝐼 ‘ 1 ) )
110 108 109 eqtrd ⊢ ( 𝜑 → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐼 ‘ 1 ) )
111 fveq1 ⊢ ( 𝑓 = ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) → ( 𝑓 ‘ 0 ) = ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 0 ) )
112 111 eqeq1d ⊢ ( 𝑓 = ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) → ( ( 𝑓 ‘ 0 ) = 𝑂 ↔ ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 0 ) = 𝑂 ) )
113 fveq1 ⊢ ( 𝑓 = ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) → ( 𝑓 ‘ 1 ) = ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 1 ) )
114 113 eqeq1d ⊢ ( 𝑓 = ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) → ( ( 𝑓 ‘ 1 ) = 𝑍 ↔ ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 1 ) = 𝑍 ) )
115 coeq2 ⊢ ( 𝑓 = ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) → ( 𝐺 ∘ 𝑓 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) )
116 115 eqeq2d ⊢ ( 𝑓 = ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) → ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ) )
117 116 anbi1d ⊢ ( 𝑓 = ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) → ( ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
118 117 riotabidv ⊢ ( 𝑓 = ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
119 118 fveq1d ⊢ ( 𝑓 = ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) )
120 119 eqeq1d ⊢ ( 𝑓 = ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐼 ‘ 1 ) ↔ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐼 ‘ 1 ) ) )
121 112 114 120 3anbi123d ⊢ ( 𝑓 = ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) → ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑍 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐼 ‘ 1 ) ) ↔ ( ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 0 ) = 𝑂 ∧ ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 1 ) = 𝑍 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐼 ‘ 1 ) ) ) )
122 121 rspcev ⊢ ( ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ∈ ( II Cn 𝐾 ) ∧ ( ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 0 ) = 𝑂 ∧ ( ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ‘ 1 ) = 𝑍 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( 𝑄 ( *𝑝 ‘ 𝐾 ) 𝑁 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐼 ‘ 1 ) ) ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑍 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐼 ‘ 1 ) ) )
123 32 35 38 110 122 syl13anc ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑍 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐼 ‘ 1 ) ) )
124 59 17 sseldd ⊢ ( 𝜑 → 𝑍 ∈ 𝑌 )
125 1 2 3 4 5 6 7 8 9 10 cvmlift3lem4 ⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝑌 ) → ( ( 𝐻 ‘ 𝑍 ) = ( 𝐼 ‘ 1 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑍 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐼 ‘ 1 ) ) ) )
126 124 125 mpdan ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑍 ) = ( 𝐼 ‘ 1 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑍 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐼 ‘ 1 ) ) ) )
127 123 126 mpbird ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑍 ) = ( 𝐼 ‘ 1 ) )
128 iiconn ⊢ II ∈ Conn
129 128 a1i ⊢ ( 𝜑 → II ∈ Conn )
130 cvmtop1 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
131 3 130 syl ⊢ ( 𝜑 → 𝐶 ∈ Top )
132 1 toptopon ⊢ ( 𝐶 ∈ Top ↔ 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
133 131 132 sylib ⊢ ( 𝜑 → 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
134 74 rneqd ⊢ ( 𝜑 → ran ( 𝐹 ∘ 𝐼 ) = ran ( 𝐺 ∘ 𝑁 ) )
135 rnco2 ⊢ ran ( 𝐹 ∘ 𝐼 ) = ( 𝐹 “ ran 𝐼 )
136 rnco2 ⊢ ran ( 𝐺 ∘ 𝑁 ) = ( 𝐺 “ ran 𝑁 )
137 134 135 136 3eqtr3g ⊢ ( 𝜑 → ( 𝐹 “ ran 𝐼 ) = ( 𝐺 “ ran 𝑁 ) )
138 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
139 138 a1i ⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
140 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
141 25 140 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
142 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑀 ⊆ 𝑌 ) → ( 𝐾 ↾t 𝑀 ) ∈ ( TopOn ‘ 𝑀 ) )
143 141 59 142 syl2anc ⊢ ( 𝜑 → ( 𝐾 ↾t 𝑀 ) ∈ ( TopOn ‘ 𝑀 ) )
144 cnf2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ ( 𝐾 ↾t 𝑀 ) ∈ ( TopOn ‘ 𝑀 ) ∧ 𝑁 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) → 𝑁 : ( 0 [,] 1 ) ⟶ 𝑀 )
145 139 143 21 144 syl3anc ⊢ ( 𝜑 → 𝑁 : ( 0 [,] 1 ) ⟶ 𝑀 )
146 145 frnd ⊢ ( 𝜑 → ran 𝑁 ⊆ 𝑀 )
147 146 14 sstrd ⊢ ( 𝜑 → ran 𝑁 ⊆ ( ◡ 𝐺 “ 𝐴 ) )
148 57 ffund ⊢ ( 𝜑 → Fun 𝐺 )
149 147 54 sstrdi ⊢ ( 𝜑 → ran 𝑁 ⊆ dom 𝐺 )
150 funimass3 ⊢ ( ( Fun 𝐺 ∧ ran 𝑁 ⊆ dom 𝐺 ) → ( ( 𝐺 “ ran 𝑁 ) ⊆ 𝐴 ↔ ran 𝑁 ⊆ ( ◡ 𝐺 “ 𝐴 ) ) )
151 148 149 150 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 “ ran 𝑁 ) ⊆ 𝐴 ↔ ran 𝑁 ⊆ ( ◡ 𝐺 “ 𝐴 ) ) )
152 147 151 mpbird ⊢ ( 𝜑 → ( 𝐺 “ ran 𝑁 ) ⊆ 𝐴 )
153 137 152 eqsstrd ⊢ ( 𝜑 → ( 𝐹 “ ran 𝐼 ) ⊆ 𝐴 )
154 1 55 cnf ⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ ∪ 𝐽 )
155 82 154 syl ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ∪ 𝐽 )
156 155 ffund ⊢ ( 𝜑 → Fun 𝐹 )
157 42 1 cnf ⊢ ( 𝐼 ∈ ( II Cn 𝐶 ) → 𝐼 : ( 0 [,] 1 ) ⟶ 𝐵 )
158 77 157 syl ⊢ ( 𝜑 → 𝐼 : ( 0 [,] 1 ) ⟶ 𝐵 )
159 158 frnd ⊢ ( 𝜑 → ran 𝐼 ⊆ 𝐵 )
160 155 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐵 )
161 159 160 sseqtrrd ⊢ ( 𝜑 → ran 𝐼 ⊆ dom 𝐹 )
162 funimass3 ⊢ ( ( Fun 𝐹 ∧ ran 𝐼 ⊆ dom 𝐹 ) → ( ( 𝐹 “ ran 𝐼 ) ⊆ 𝐴 ↔ ran 𝐼 ⊆ ( ◡ 𝐹 “ 𝐴 ) ) )
163 156 161 162 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 “ ran 𝐼 ) ⊆ 𝐴 ↔ ran 𝐼 ⊆ ( ◡ 𝐹 “ 𝐴 ) ) )
164 153 163 mpbid ⊢ ( 𝜑 → ran 𝐼 ⊆ ( ◡ 𝐹 “ 𝐴 ) )
165 cnvimass ⊢ ( ◡ 𝐹 “ 𝐴 ) ⊆ dom 𝐹
166 165 155 fssdm ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝐴 ) ⊆ 𝐵 )
167 cnrest2 ⊢ ( ( 𝐶 ∈ ( TopOn ‘ 𝐵 ) ∧ ran 𝐼 ⊆ ( ◡ 𝐹 “ 𝐴 ) ∧ ( ◡ 𝐹 “ 𝐴 ) ⊆ 𝐵 ) → ( 𝐼 ∈ ( II Cn 𝐶 ) ↔ 𝐼 ∈ ( II Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝐴 ) ) ) ) )
168 133 164 166 167 syl3anc ⊢ ( 𝜑 → ( 𝐼 ∈ ( II Cn 𝐶 ) ↔ 𝐼 ∈ ( II Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝐴 ) ) ) ) )
169 77 168 mpbid ⊢ ( 𝜑 → 𝐼 ∈ ( II Cn ( 𝐶 ↾t ( ◡ 𝐹 “ 𝐴 ) ) ) )
170 11 cvmsss ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) → 𝑇 ⊆ 𝐶 )
171 13 170 syl ⊢ ( 𝜑 → 𝑇 ⊆ 𝐶 )
172 71 12 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) ∈ 𝐴 )
173 11 1 15 cvmsiota ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) ∈ 𝐴 ) ) → ( 𝑊 ∈ 𝑇 ∧ ( 𝐻 ‘ 𝑋 ) ∈ 𝑊 ) )
174 3 13 61 172 173 syl13anc ⊢ ( 𝜑 → ( 𝑊 ∈ 𝑇 ∧ ( 𝐻 ‘ 𝑋 ) ∈ 𝑊 ) )
175 174 simpld ⊢ ( 𝜑 → 𝑊 ∈ 𝑇 )
176 171 175 sseldd ⊢ ( 𝜑 → 𝑊 ∈ 𝐶 )
177 elssuni ⊢ ( 𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇 )
178 175 177 syl ⊢ ( 𝜑 → 𝑊 ⊆ ∪ 𝑇 )
179 11 cvmsuni ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) → ∪ 𝑇 = ( ◡ 𝐹 “ 𝐴 ) )
180 13 179 syl ⊢ ( 𝜑 → ∪ 𝑇 = ( ◡ 𝐹 “ 𝐴 ) )
181 178 180 sseqtrd ⊢ ( 𝜑 → 𝑊 ⊆ ( ◡ 𝐹 “ 𝐴 ) )
182 11 cvmsrcl ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) → 𝐴 ∈ 𝐽 )
183 13 182 syl ⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
184 cnima ⊢ ( ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ∧ 𝐴 ∈ 𝐽 ) → ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐶 )
185 82 183 184 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐶 )
186 restopn2 ⊢ ( ( 𝐶 ∈ Top ∧ ( ◡ 𝐹 “ 𝐴 ) ∈ 𝐶 ) → ( 𝑊 ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝐴 ) ) ↔ ( 𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ ( ◡ 𝐹 “ 𝐴 ) ) ) )
187 131 185 186 syl2anc ⊢ ( 𝜑 → ( 𝑊 ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝐴 ) ) ↔ ( 𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ ( ◡ 𝐹 “ 𝐴 ) ) ) )
188 176 181 187 mpbir2and ⊢ ( 𝜑 → 𝑊 ∈ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝐴 ) ) )
189 11 cvmscld ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) ∧ 𝑊 ∈ 𝑇 ) → 𝑊 ∈ ( Clsd ‘ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝐴 ) ) ) )
190 3 13 175 189 syl3anc ⊢ ( 𝜑 → 𝑊 ∈ ( Clsd ‘ ( 𝐶 ↾t ( ◡ 𝐹 “ 𝐴 ) ) ) )
191 45 a1i ⊢ ( 𝜑 → 0 ∈ ( 0 [,] 1 ) )
192 174 simprd ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) ∈ 𝑊 )
193 79 192 eqeltrd ⊢ ( 𝜑 → ( 𝐼 ‘ 0 ) ∈ 𝑊 )
194 42 129 169 188 190 191 193 conncn ⊢ ( 𝜑 → 𝐼 : ( 0 [,] 1 ) ⟶ 𝑊 )
195 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
196 ffvelcdm ⊢ ( ( 𝐼 : ( 0 [,] 1 ) ⟶ 𝑊 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝐼 ‘ 1 ) ∈ 𝑊 )
197 194 195 196 sylancl ⊢ ( 𝜑 → ( 𝐼 ‘ 1 ) ∈ 𝑊 )
198 127 197 eqeltrd ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑍 ) ∈ 𝑊 )