Metamath Proof Explorer

Theorem cvmlift3lem7

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 ⊢ 𝑊 = ( ℩ 𝑏 ∈ 𝑇 ( 𝐻 ‘ 𝑋 ) ∈ 𝑏 )
cvmlift3lem7.7 ⊢ ( 𝜑 → ( 𝐾 ↾t 𝑀 ) ∈ PConn )
cvmlift3lem7.4 ⊢ ( 𝜑 → 𝑉 ∈ 𝐾 )
cvmlift3lem7.5 ⊢ ( 𝜑 → 𝑉 ⊆ 𝑀 )
cvmlift3lem7.6 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion cvmlift3lem7 ( 𝜑 → 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑋 ) )

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 cvmlift3lem7.7 ⊢ ( 𝜑 → ( 𝐾 ↾t 𝑀 ) ∈ PConn )
17 cvmlift3lem7.4 ⊢ ( 𝜑 → 𝑉 ∈ 𝐾 )
18 cvmlift3lem7.5 ⊢ ( 𝜑 → 𝑉 ⊆ 𝑀 )
19 cvmlift3lem7.6 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
20 1 2 3 4 5 6 7 8 9 10 cvmlift3lem3 ⊢ ( 𝜑 → 𝐻 : 𝑌 ⟶ 𝐵 )
21 1 2 3 4 5 6 7 8 9 10 cvmlift3lem5 ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) = 𝐺 )
22 21 7 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) ∈ ( 𝐾 Cn 𝐽 ) )
23 sconntop ⊢ ( 𝐾 ∈ SConn → 𝐾 ∈ Top )
24 4 23 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
25 cnvimass ⊢ ( ◡ 𝐺 “ 𝐴 ) ⊆ dom 𝐺
26 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
27 2 26 cnf ⊢ ( 𝐺 ∈ ( 𝐾 Cn 𝐽 ) → 𝐺 : 𝑌 ⟶ ∪ 𝐽 )
28 fdm ⊢ ( 𝐺 : 𝑌 ⟶ ∪ 𝐽 → dom 𝐺 = 𝑌 )
29 7 27 28 3syl ⊢ ( 𝜑 → dom 𝐺 = 𝑌 )
30 25 29 sseqtrid ⊢ ( 𝜑 → ( ◡ 𝐺 “ 𝐴 ) ⊆ 𝑌 )
31 14 30 sstrd ⊢ ( 𝜑 → 𝑀 ⊆ 𝑌 )
32 18 19 sseldd ⊢ ( 𝜑 → 𝑋 ∈ 𝑀 )
33 31 32 sseldd ⊢ ( 𝜑 → 𝑋 ∈ 𝑌 )
34 20 33 ffvelcdmd ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) ∈ 𝐵 )
35 fvco3 ⊢ ( ( 𝐻 : 𝑌 ⟶ 𝐵 ∧ 𝑋 ∈ 𝑌 ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) )
36 20 33 35 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) )
37 21 fveq1d ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
38 36 37 eqtr3d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) = ( 𝐺 ‘ 𝑋 ) )
39 38 12 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) ∈ 𝐴 )
40 11 1 15 cvmsiota ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) ∧ ( 𝐻 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) ∈ 𝐴 ) ) → ( 𝑊 ∈ 𝑇 ∧ ( 𝐻 ‘ 𝑋 ) ∈ 𝑊 ) )
41 3 13 34 39 40 syl13anc ⊢ ( 𝜑 → ( 𝑊 ∈ 𝑇 ∧ ( 𝐻 ‘ 𝑋 ) ∈ 𝑊 ) )
42 eqid ⊢ ( 𝐻 ‘ 𝑋 ) = ( 𝐻 ‘ 𝑋 )
43 1 2 3 4 5 6 7 8 9 10 cvmlift3lem4 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ( ( 𝐻 ‘ 𝑋 ) = ( 𝐻 ‘ 𝑋 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ) )
44 42 43 mpbii ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) )
45 33 44 mpdan ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) )
47 fveq1 ⊢ ( 𝑓 = ℎ → ( 𝑓 ‘ 0 ) = ( ℎ ‘ 0 ) )
48 47 eqeq1d ⊢ ( 𝑓 = ℎ → ( ( 𝑓 ‘ 0 ) = 𝑂 ↔ ( ℎ ‘ 0 ) = 𝑂 ) )
49 fveq1 ⊢ ( 𝑓 = ℎ → ( 𝑓 ‘ 1 ) = ( ℎ ‘ 1 ) )
50 49 eqeq1d ⊢ ( 𝑓 = ℎ → ( ( 𝑓 ‘ 1 ) = 𝑋 ↔ ( ℎ ‘ 1 ) = 𝑋 ) )
51 coeq2 ⊢ ( 𝑓 = ℎ → ( 𝐺 ∘ 𝑓 ) = ( 𝐺 ∘ ℎ ) )
52 51 eqeq2d ⊢ ( 𝑓 = ℎ → ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ) )
53 52 anbi1d ⊢ ( 𝑓 = ℎ → ( ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
54 53 riotabidv ⊢ ( 𝑓 = ℎ → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
55 coeq2 ⊢ ( 𝑎 = 𝑔 → ( 𝐹 ∘ 𝑎 ) = ( 𝐹 ∘ 𝑔 ) )
56 55 eqeq1d ⊢ ( 𝑎 = 𝑔 → ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ) )
57 fveq1 ⊢ ( 𝑎 = 𝑔 → ( 𝑎 ‘ 0 ) = ( 𝑔 ‘ 0 ) )
58 57 eqeq1d ⊢ ( 𝑎 = 𝑔 → ( ( 𝑎 ‘ 0 ) = 𝑃 ↔ ( 𝑔 ‘ 0 ) = 𝑃 ) )
59 56 58 anbi12d ⊢ ( 𝑎 = 𝑔 → ( ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
60 59 cbvriotavw ⊢ ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
61 54 60 eqtr4di ⊢ ( 𝑓 = ℎ → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) )
62 61 fveq1d ⊢ ( 𝑓 = ℎ → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) )
63 62 eqeq1d ⊢ ( 𝑓 = ℎ → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ↔ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) )
64 48 50 63 3anbi123d ⊢ ( 𝑓 = ℎ → ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ↔ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ) )
65 64 cbvrexvw ⊢ ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ↔ ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) )
66 46 65 sylib ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) )
67 16 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝐾 ↾t 𝑀 ) ∈ PConn )
68 2 restuni ⊢ ( ( 𝐾 ∈ Top ∧ 𝑀 ⊆ 𝑌 ) → 𝑀 = ∪ ( 𝐾 ↾t 𝑀 ) )
69 24 31 68 syl2anc ⊢ ( 𝜑 → 𝑀 = ∪ ( 𝐾 ↾t 𝑀 ) )
70 32 69 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ∪ ( 𝐾 ↾t 𝑀 ) )
71 70 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑋 ∈ ∪ ( 𝐾 ↾t 𝑀 ) )
72 69 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑀 ↔ 𝑦 ∈ ∪ ( 𝐾 ↾t 𝑀 ) ) )
73 72 biimpa ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ ∪ ( 𝐾 ↾t 𝑀 ) )
74 eqid ⊢ ∪ ( 𝐾 ↾t 𝑀 ) = ∪ ( 𝐾 ↾t 𝑀 )
75 74 pconncn ⊢ ( ( ( 𝐾 ↾t 𝑀 ) ∈ PConn ∧ 𝑋 ∈ ∪ ( 𝐾 ↾t 𝑀 ) ∧ 𝑦 ∈ ∪ ( 𝐾 ↾t 𝑀 ) ) → ∃ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) )
76 67 71 73 75 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ∃ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) )
77 reeanv ⊢ ( ∃ ℎ ∈ ( II Cn 𝐾 ) ∃ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ↔ ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ∃ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) )
78 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
79 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → 𝐾 ∈ SConn )
80 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → 𝐾 ∈ 𝑛-Locally PConn )
81 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → 𝑂 ∈ 𝑌 )
82 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
83 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → 𝑃 ∈ 𝐵 )
84 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
85 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → ( 𝐺 ‘ 𝑋 ) ∈ 𝐴 )
86 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) )
87 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → 𝑀 ⊆ ( ◡ 𝐺 “ 𝐴 ) )
88 32 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → 𝑋 ∈ 𝑀 )
89 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → 𝑦 ∈ 𝑀 )
90 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → ℎ ∈ ( II Cn 𝐾 ) )
91 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) )
92 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) )
93 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) )
94 55 eqeq1d ⊢ ( 𝑎 = 𝑔 → ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ 𝑛 ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑛 ) ) )
95 57 eqeq1d ⊢ ( 𝑎 = 𝑔 → ( ( 𝑎 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ↔ ( 𝑔 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )
96 94 95 anbi12d ⊢ ( 𝑎 = 𝑔 → ( ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ 𝑛 ) ∧ ( 𝑎 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ↔ ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑛 ) ∧ ( 𝑔 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) )
97 96 cbvriotavw ⊢ ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ 𝑛 ) ∧ ( 𝑎 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑛 ) ∧ ( 𝑔 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )
98 1 2 78 79 80 81 82 83 84 10 11 85 86 87 15 88 89 90 60 91 92 93 97 cvmlift3lem6 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) ∧ ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝑊 )
99 98 ex ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ) ) → ( ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝑊 ) )
100 99 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ∃ ℎ ∈ ( II Cn 𝐾 ) ∃ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝑊 ) )
101 77 100 biimtrrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑎 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑎 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑎 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑋 ) ) ∧ ∃ 𝑛 ∈ ( II Cn ( 𝐾 ↾t 𝑀 ) ) ( ( 𝑛 ‘ 0 ) = 𝑋 ∧ ( 𝑛 ‘ 1 ) = 𝑦 ) ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝑊 ) )
102 66 76 101 mp2and ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝑊 )
103 102 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑀 ( 𝐻 ‘ 𝑦 ) ∈ 𝑊 )
104 20 ffund ⊢ ( 𝜑 → Fun 𝐻 )
105 20 fdmd ⊢ ( 𝜑 → dom 𝐻 = 𝑌 )
106 31 105 sseqtrrd ⊢ ( 𝜑 → 𝑀 ⊆ dom 𝐻 )
107 funimass4 ⊢ ( ( Fun 𝐻 ∧ 𝑀 ⊆ dom 𝐻 ) → ( ( 𝐻 “ 𝑀 ) ⊆ 𝑊 ↔ ∀ 𝑦 ∈ 𝑀 ( 𝐻 ‘ 𝑦 ) ∈ 𝑊 ) )
108 104 106 107 syl2anc ⊢ ( 𝜑 → ( ( 𝐻 “ 𝑀 ) ⊆ 𝑊 ↔ ∀ 𝑦 ∈ 𝑀 ( 𝐻 ‘ 𝑦 ) ∈ 𝑊 ) )
109 103 108 mpbird ⊢ ( 𝜑 → ( 𝐻 “ 𝑀 ) ⊆ 𝑊 )
110 1 2 11 3 20 22 24 33 13 41 31 109 cvmlift2lem9a ⊢ ( 𝜑 → ( 𝐻 ↾ 𝑀 ) ∈ ( ( 𝐾 ↾t 𝑀 ) Cn 𝐶 ) )
111 74 cncnpi ⊢ ( ( ( 𝐻 ↾ 𝑀 ) ∈ ( ( 𝐾 ↾t 𝑀 ) Cn 𝐶 ) ∧ 𝑋 ∈ ∪ ( 𝐾 ↾t 𝑀 ) ) → ( 𝐻 ↾ 𝑀 ) ∈ ( ( ( 𝐾 ↾t 𝑀 ) CnP 𝐶 ) ‘ 𝑋 ) )
112 110 70 111 syl2anc ⊢ ( 𝜑 → ( 𝐻 ↾ 𝑀 ) ∈ ( ( ( 𝐾 ↾t 𝑀 ) CnP 𝐶 ) ‘ 𝑋 ) )
113 2 ssntr ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝑀 ⊆ 𝑌 ) ∧ ( 𝑉 ∈ 𝐾 ∧ 𝑉 ⊆ 𝑀 ) ) → 𝑉 ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑀 ) )
114 24 31 17 18 113 syl22anc ⊢ ( 𝜑 → 𝑉 ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑀 ) )
115 114 19 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ( ( int ‘ 𝐾 ) ‘ 𝑀 ) )
116 2 1 cnprest ⊢ ( ( ( 𝐾 ∈ Top ∧ 𝑀 ⊆ 𝑌 ) ∧ ( 𝑋 ∈ ( ( int ‘ 𝐾 ) ‘ 𝑀 ) ∧ 𝐻 : 𝑌 ⟶ 𝐵 ) ) → ( 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑋 ) ↔ ( 𝐻 ↾ 𝑀 ) ∈ ( ( ( 𝐾 ↾t 𝑀 ) CnP 𝐶 ) ‘ 𝑋 ) ) )
117 24 31 115 20 116 syl22anc ⊢ ( 𝜑 → ( 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑋 ) ↔ ( 𝐻 ↾ 𝑀 ) ∈ ( ( ( 𝐾 ↾t 𝑀 ) CnP 𝐶 ) ‘ 𝑋 ) ) )
118 112 117 mpbird ⊢ ( 𝜑 → 𝐻 ∈ ( ( 𝐾 CnP 𝐶 ) ‘ 𝑋 ) )