Metamath Proof Explorer

Theorem cvmlift2lem9a

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

Ref Expression
Hypotheses cvmlift2lem9a.b ⊢ 𝐵 = ∪ 𝐶
cvmlift2lem9a.y ⊢ 𝑌 = ∪ 𝐾
cvmlift2lem9a.s ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
cvmlift2lem9a.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmlift2lem9a.h ⊢ ( 𝜑 → 𝐻 : 𝑌 ⟶ 𝐵 )
cvmlift2lem9a.g ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) ∈ ( 𝐾 Cn 𝐽 ) )
cvmlift2lem9a.k ⊢ ( 𝜑 → 𝐾 ∈ Top )
cvmlift2lem9a.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑌 )
cvmlift2lem9a.2 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) )
cvmlift2lem9a.3 ⊢ ( 𝜑 → ( 𝑊 ∈ 𝑇 ∧ ( 𝐻 ‘ 𝑋 ) ∈ 𝑊 ) )
cvmlift2lem9a.4 ⊢ ( 𝜑 → 𝑀 ⊆ 𝑌 )
cvmlift2lem9a.6 ⊢ ( 𝜑 → ( 𝐻 “ 𝑀 ) ⊆ 𝑊 )
Assertion cvmlift2lem9a ( 𝜑 → ( 𝐻 ↾ 𝑀 ) ∈ ( ( 𝐾 ↾t 𝑀 ) Cn 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cvmlift2lem9a.b ⊢ 𝐵 = ∪ 𝐶
2 cvmlift2lem9a.y ⊢ 𝑌 = ∪ 𝐾
3 cvmlift2lem9a.s ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
4 cvmlift2lem9a.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
5 cvmlift2lem9a.h ⊢ ( 𝜑 → 𝐻 : 𝑌 ⟶ 𝐵 )
6 cvmlift2lem9a.g ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) ∈ ( 𝐾 Cn 𝐽 ) )
7 cvmlift2lem9a.k ⊢ ( 𝜑 → 𝐾 ∈ Top )
8 cvmlift2lem9a.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑌 )
9 cvmlift2lem9a.2 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) )
10 cvmlift2lem9a.3 ⊢ ( 𝜑 → ( 𝑊 ∈ 𝑇 ∧ ( 𝐻 ‘ 𝑋 ) ∈ 𝑊 ) )
11 cvmlift2lem9a.4 ⊢ ( 𝜑 → 𝑀 ⊆ 𝑌 )
12 cvmlift2lem9a.6 ⊢ ( 𝜑 → ( 𝐻 “ 𝑀 ) ⊆ 𝑊 )
13 cvmtop1 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
14 4 13 syl ⊢ ( 𝜑 → 𝐶 ∈ Top )
15 cnrest2r ⊢ ( 𝐶 ∈ Top → ( ( 𝐾 ↾t 𝑀 ) Cn ( 𝐶 ↾t 𝑊 ) ) ⊆ ( ( 𝐾 ↾t 𝑀 ) Cn 𝐶 ) )
16 14 15 syl ⊢ ( 𝜑 → ( ( 𝐾 ↾t 𝑀 ) Cn ( 𝐶 ↾t 𝑊 ) ) ⊆ ( ( 𝐾 ↾t 𝑀 ) Cn 𝐶 ) )
17 5 ffnd ⊢ ( 𝜑 → 𝐻 Fn 𝑌 )
18 fnssres ⊢ ( ( 𝐻 Fn 𝑌 ∧ 𝑀 ⊆ 𝑌 ) → ( 𝐻 ↾ 𝑀 ) Fn 𝑀 )
19 17 11 18 syl2anc ⊢ ( 𝜑 → ( 𝐻 ↾ 𝑀 ) Fn 𝑀 )
20 df-ima ⊢ ( 𝐻 “ 𝑀 ) = ran ( 𝐻 ↾ 𝑀 )
21 20 12 eqsstrrid ⊢ ( 𝜑 → ran ( 𝐻 ↾ 𝑀 ) ⊆ 𝑊 )
22 df-f ⊢ ( ( 𝐻 ↾ 𝑀 ) : 𝑀 ⟶ 𝑊 ↔ ( ( 𝐻 ↾ 𝑀 ) Fn 𝑀 ∧ ran ( 𝐻 ↾ 𝑀 ) ⊆ 𝑊 ) )
23 19 21 22 sylanbrc ⊢ ( 𝜑 → ( 𝐻 ↾ 𝑀 ) : 𝑀 ⟶ 𝑊 )
24 10 simpld ⊢ ( 𝜑 → 𝑊 ∈ 𝑇 )
25 3 cvmsf1o ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) ∧ 𝑊 ∈ 𝑇 ) → ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1-onto→ 𝐴 )
26 4 9 24 25 syl3anc ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1-onto→ 𝐴 )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1-onto→ 𝐴 )
28 f1of1 ⊢ ( ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1-onto→ 𝐴 → ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1→ 𝐴 )
29 27 28 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1→ 𝐴 )
30 1 toptopon ⊢ ( 𝐶 ∈ Top ↔ 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
31 14 30 sylib ⊢ ( 𝜑 → 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
32 3 cvmsss ⊢ ( 𝑇 ∈ ( 𝑆 ‘ 𝐴 ) → 𝑇 ⊆ 𝐶 )
33 9 32 syl ⊢ ( 𝜑 → 𝑇 ⊆ 𝐶 )
34 33 24 sseldd ⊢ ( 𝜑 → 𝑊 ∈ 𝐶 )
35 toponss ⊢ ( ( 𝐶 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝑊 ∈ 𝐶 ) → 𝑊 ⊆ 𝐵 )
36 31 34 35 syl2anc ⊢ ( 𝜑 → 𝑊 ⊆ 𝐵 )
37 resttopon ⊢ ( ( 𝐶 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝑊 ⊆ 𝐵 ) → ( 𝐶 ↾t 𝑊 ) ∈ ( TopOn ‘ 𝑊 ) )
38 31 36 37 syl2anc ⊢ ( 𝜑 → ( 𝐶 ↾t 𝑊 ) ∈ ( TopOn ‘ 𝑊 ) )
39 toponss ⊢ ( ( ( 𝐶 ↾t 𝑊 ) ∈ ( TopOn ‘ 𝑊 ) ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → 𝑥 ⊆ 𝑊 )
40 38 39 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → 𝑥 ⊆ 𝑊 )
41 f1imacnv ⊢ ( ( ( 𝐹 ↾ 𝑊 ) : 𝑊 –1-1→ 𝐴 ∧ 𝑥 ⊆ 𝑊 ) → ( ◡ ( 𝐹 ↾ 𝑊 ) “ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ) = 𝑥 )
42 29 40 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( ◡ ( 𝐹 ↾ 𝑊 ) “ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ) = 𝑥 )
43 42 imaeq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( ◡ ( 𝐻 ↾ 𝑀 ) “ ( ◡ ( 𝐹 ↾ 𝑊 ) “ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ) ) = ( ◡ ( 𝐻 ↾ 𝑀 ) “ 𝑥 ) )
44 imaco ⊢ ( ( ◡ ( 𝐻 ↾ 𝑀 ) ∘ ◡ ( 𝐹 ↾ 𝑊 ) ) “ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ) = ( ◡ ( 𝐻 ↾ 𝑀 ) “ ( ◡ ( 𝐹 ↾ 𝑊 ) “ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ) )
45 cnvco ⊢ ◡ ( ( 𝐹 ↾ 𝑊 ) ∘ ( 𝐻 ↾ 𝑀 ) ) = ( ◡ ( 𝐻 ↾ 𝑀 ) ∘ ◡ ( 𝐹 ↾ 𝑊 ) )
46 cores ⊢ ( ran ( 𝐻 ↾ 𝑀 ) ⊆ 𝑊 → ( ( 𝐹 ↾ 𝑊 ) ∘ ( 𝐻 ↾ 𝑀 ) ) = ( 𝐹 ∘ ( 𝐻 ↾ 𝑀 ) ) )
47 21 46 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝑊 ) ∘ ( 𝐻 ↾ 𝑀 ) ) = ( 𝐹 ∘ ( 𝐻 ↾ 𝑀 ) ) )
48 resco ⊢ ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) = ( 𝐹 ∘ ( 𝐻 ↾ 𝑀 ) )
49 47 48 eqtr4di ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝑊 ) ∘ ( 𝐻 ↾ 𝑀 ) ) = ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( ( 𝐹 ↾ 𝑊 ) ∘ ( 𝐻 ↾ 𝑀 ) ) = ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) )
51 50 cnveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ◡ ( ( 𝐹 ↾ 𝑊 ) ∘ ( 𝐻 ↾ 𝑀 ) ) = ◡ ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) )
52 45 51 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( ◡ ( 𝐻 ↾ 𝑀 ) ∘ ◡ ( 𝐹 ↾ 𝑊 ) ) = ◡ ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) )
53 52 imaeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( ( ◡ ( 𝐻 ↾ 𝑀 ) ∘ ◡ ( 𝐹 ↾ 𝑊 ) ) “ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ) = ( ◡ ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) “ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ) )
54 44 53 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( ◡ ( 𝐻 ↾ 𝑀 ) “ ( ◡ ( 𝐹 ↾ 𝑊 ) “ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ) ) = ( ◡ ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) “ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ) )
55 43 54 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( ◡ ( 𝐻 ↾ 𝑀 ) “ 𝑥 ) = ( ◡ ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) “ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ) )
56 2 cnrest ⊢ ( ( ( 𝐹 ∘ 𝐻 ) ∈ ( 𝐾 Cn 𝐽 ) ∧ 𝑀 ⊆ 𝑌 ) → ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) ∈ ( ( 𝐾 ↾t 𝑀 ) Cn 𝐽 ) )
57 6 11 56 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) ∈ ( ( 𝐾 ↾t 𝑀 ) Cn 𝐽 ) )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) ∈ ( ( 𝐾 ↾t 𝑀 ) Cn 𝐽 ) )
59 resima2 ⊢ ( 𝑥 ⊆ 𝑊 → ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) = ( 𝐹 “ 𝑥 ) )
60 40 59 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) = ( 𝐹 “ 𝑥 ) )
61 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
62 restopn2 ⊢ ( ( 𝐶 ∈ Top ∧ 𝑊 ∈ 𝐶 ) → ( 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ⊆ 𝑊 ) ) )
63 14 34 62 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ⊆ 𝑊 ) ) )
64 63 simprbda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → 𝑥 ∈ 𝐶 )
65 cvmopn ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 “ 𝑥 ) ∈ 𝐽 )
66 61 64 65 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( 𝐹 “ 𝑥 ) ∈ 𝐽 )
67 60 66 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ∈ 𝐽 )
68 cnima ⊢ ( ( ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) ∈ ( ( 𝐾 ↾t 𝑀 ) Cn 𝐽 ) ∧ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ∈ 𝐽 ) → ( ◡ ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) “ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ) ∈ ( 𝐾 ↾t 𝑀 ) )
69 58 67 68 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( ◡ ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑀 ) “ ( ( 𝐹 ↾ 𝑊 ) “ 𝑥 ) ) ∈ ( 𝐾 ↾t 𝑀 ) )
70 55 69 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ) → ( ◡ ( 𝐻 ↾ 𝑀 ) “ 𝑥 ) ∈ ( 𝐾 ↾t 𝑀 ) )
71 70 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ( ◡ ( 𝐻 ↾ 𝑀 ) “ 𝑥 ) ∈ ( 𝐾 ↾t 𝑀 ) )
72 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
73 7 72 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
74 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑀 ⊆ 𝑌 ) → ( 𝐾 ↾t 𝑀 ) ∈ ( TopOn ‘ 𝑀 ) )
75 73 11 74 syl2anc ⊢ ( 𝜑 → ( 𝐾 ↾t 𝑀 ) ∈ ( TopOn ‘ 𝑀 ) )
76 iscn ⊢ ( ( ( 𝐾 ↾t 𝑀 ) ∈ ( TopOn ‘ 𝑀 ) ∧ ( 𝐶 ↾t 𝑊 ) ∈ ( TopOn ‘ 𝑊 ) ) → ( ( 𝐻 ↾ 𝑀 ) ∈ ( ( 𝐾 ↾t 𝑀 ) Cn ( 𝐶 ↾t 𝑊 ) ) ↔ ( ( 𝐻 ↾ 𝑀 ) : 𝑀 ⟶ 𝑊 ∧ ∀ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ( ◡ ( 𝐻 ↾ 𝑀 ) “ 𝑥 ) ∈ ( 𝐾 ↾t 𝑀 ) ) ) )
77 75 38 76 syl2anc ⊢ ( 𝜑 → ( ( 𝐻 ↾ 𝑀 ) ∈ ( ( 𝐾 ↾t 𝑀 ) Cn ( 𝐶 ↾t 𝑊 ) ) ↔ ( ( 𝐻 ↾ 𝑀 ) : 𝑀 ⟶ 𝑊 ∧ ∀ 𝑥 ∈ ( 𝐶 ↾t 𝑊 ) ( ◡ ( 𝐻 ↾ 𝑀 ) “ 𝑥 ) ∈ ( 𝐾 ↾t 𝑀 ) ) ) )
78 23 71 77 mpbir2and ⊢ ( 𝜑 → ( 𝐻 ↾ 𝑀 ) ∈ ( ( 𝐾 ↾t 𝑀 ) Cn ( 𝐶 ↾t 𝑊 ) ) )
79 16 78 sseldd ⊢ ( 𝜑 → ( 𝐻 ↾ 𝑀 ) ∈ ( ( 𝐾 ↾t 𝑀 ) Cn 𝐶 ) )