Metamath Proof Explorer

Theorem cvmlift3lem8

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 6-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 𝑘 ) ) ) ) } )
Assertion cvmlift3lem8 ( 𝜑 → 𝐻 ∈ ( 𝐾 Cn 𝐶 ) )

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 1 2 3 4 5 6 7 8 9 10 cvmlift3lem3 ⊢ ( 𝜑 → 𝐻 : 𝑌 ⟶ 𝐵 )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
14 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
15 2 14 cnf ⊢ ( 𝐺 ∈ ( 𝐾 Cn 𝐽 ) → 𝐺 : 𝑌 ⟶ ∪ 𝐽 )
16 7 15 syl ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ∪ 𝐽 )
17 16 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑦 ) ∈ ∪ 𝐽 )
18 11 14 cvmcov ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ ∪ 𝐽 ) → ∃ 𝑎 ∈ 𝐽 ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ ( 𝑆 ‘ 𝑎 ) ≠ ∅ ) )
19 13 17 18 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ∃ 𝑎 ∈ 𝐽 ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ ( 𝑆 ‘ 𝑎 ) ≠ ∅ ) )
20 n0 ⊢ ( ( 𝑆 ‘ 𝑎 ) ≠ ∅ ↔ ∃ 𝑡 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) )
21 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → 𝐾 ∈ 𝑛-Locally PConn )
22 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
23 simprr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) )
24 11 cvmsrcl ⊢ ( 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) → 𝑎 ∈ 𝐽 )
25 23 24 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → 𝑎 ∈ 𝐽 )
26 cnima ⊢ ( ( 𝐺 ∈ ( 𝐾 Cn 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) → ( ◡ 𝐺 “ 𝑎 ) ∈ 𝐾 )
27 22 25 26 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → ( ◡ 𝐺 “ 𝑎 ) ∈ 𝐾 )
28 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → 𝑦 ∈ 𝑌 )
29 simprl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 )
30 ffn ⊢ ( 𝐺 : 𝑌 ⟶ ∪ 𝐽 → 𝐺 Fn 𝑌 )
31 elpreima ⊢ ( 𝐺 Fn 𝑌 → ( 𝑦 ∈ ( ◡ 𝐺 “ 𝑎 ) ↔ ( 𝑦 ∈ 𝑌 ∧ ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ) ) )
32 22 15 30 31 4syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → ( 𝑦 ∈ ( ◡ 𝐺 “ 𝑎 ) ↔ ( 𝑦 ∈ 𝑌 ∧ ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ) ) )
33 28 29 32 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → 𝑦 ∈ ( ◡ 𝐺 “ 𝑎 ) )
34 nlly2i ⊢ ( ( 𝐾 ∈ 𝑛-Locally PConn ∧ ( ◡ 𝐺 “ 𝑎 ) ∈ 𝐾 ∧ 𝑦 ∈ ( ◡ 𝐺 “ 𝑎 ) ) → ∃ 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∃ 𝑣 ∈ 𝐾 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) )
35 21 27 33 34 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → ∃ 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∃ 𝑣 ∈ 𝐾 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) )
36 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
37 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝐾 ∈ SConn )
38 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝐾 ∈ 𝑛-Locally PConn )
39 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝑂 ∈ 𝑌 )
40 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
41 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝑃 ∈ 𝐵 )
42 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
43 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 )
44 23 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) )
45 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) )
46 45 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝑚 ⊆ ( ◡ 𝐺 “ 𝑎 ) )
47 eqid ⊢ ( ℩ 𝑏 ∈ 𝑡 ( 𝐻 ‘ 𝑦 ) ∈ 𝑏 ) = ( ℩ 𝑏 ∈ 𝑡 ( 𝐻 ‘ 𝑦 ) ∈ 𝑏 )
48 simprr3 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → ( 𝐾 ↾t 𝑚 ) ∈ PConn )
49 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝑣 ∈ 𝐾 )
50 simprr2 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝑣 ⊆ 𝑚 )
51 simprr1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝑦 ∈ 𝑣 )
52 1 2 36 37 38 39 40 41 42 10 11 43 44 46 47 48 49 50 51 cvmlift3lem7 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ∧ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) ) ) → 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) )
53 52 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) ∧ ( 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∧ 𝑣 ∈ 𝐾 ) ) → ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) → 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) ) )
54 53 rexlimdvva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → ( ∃ 𝑚 ∈ 𝒫 ( ◡ 𝐺 “ 𝑎 ) ∃ 𝑣 ∈ 𝐾 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑚 ∧ ( 𝐾 ↾t 𝑚 ) ∈ PConn ) → 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) ) )
55 35 54 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) ) ) → 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) )
56 55 expr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ) → ( 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) → 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) ) )
57 56 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ) → ( ∃ 𝑡 𝑡 ∈ ( 𝑆 ‘ 𝑎 ) → 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) ) )
58 20 57 biimtrid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ) → ( ( 𝑆 ‘ 𝑎 ) ≠ ∅ → 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) ) )
59 58 expimpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ ( 𝑆 ‘ 𝑎 ) ≠ ∅ ) → 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) ) )
60 59 rexlimdvw ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( ∃ 𝑎 ∈ 𝐽 ( ( 𝐺 ‘ 𝑦 ) ∈ 𝑎 ∧ ( 𝑆 ‘ 𝑎 ) ≠ ∅ ) → 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) ) )
61 19 60 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) )
62 61 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑌 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) )
63 sconntop ⊢ ( 𝐾 ∈ SConn → 𝐾 ∈ Top )
64 4 63 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
65 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
66 64 65 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
67 cvmtop1 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
68 3 67 syl ⊢ ( 𝜑 → 𝐶 ∈ Top )
69 1 toptopon ⊢ ( 𝐶 ∈ Top ↔ 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
70 68 69 sylib ⊢ ( 𝜑 → 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
71 cncnp ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐶 ∈ ( TopOn ‘ 𝐵 ) ) → ( 𝐻 ∈ ( 𝐾 Cn 𝐶 ) ↔ ( 𝐻 : 𝑌 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝑌 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) ) ) )
72 66 70 71 syl2anc ⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝐾 Cn 𝐶 ) ↔ ( 𝐻 : 𝑌 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝑌 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑦 ) ) ) )
73 12 62 72 mpbir2and ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐾 Cn 𝐶 ) )