Metamath Proof Explorer

Theorem cvmlift3lem1

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

Ref Expression
Hypotheses cvmlift3.b ⊢ B = ⋃ C
cvmlift3.y ⊢ Y = ⋃ K
cvmlift3.f ⊢ φ → F ∈ C CovMap J
cvmlift3.k ⊢ φ → K ∈ SConn
cvmlift3.l ⊢ φ → K ∈ N-Locally PConn
cvmlift3.o ⊢ φ → O ∈ Y
cvmlift3.g ⊢ φ → G ∈ K Cn J
cvmlift3.p ⊢ φ → P ∈ B
cvmlift3.e ⊢ φ → F ⁡ P = G ⁡ O
cvmlift3lem1.1 ⊢ φ → M ∈ II Cn K
cvmlift3lem1.2 ⊢ φ → M ⁡ 0 = O
cvmlift3lem1.3 ⊢ φ → N ∈ II Cn K
cvmlift3lem1.4 ⊢ φ → N ⁡ 0 = O
cvmlift3lem1.5 ⊢ φ → M ⁡ 1 = N ⁡ 1
Assertion cvmlift3lem1 ⊢ φ → ι g ∈ II Cn C | F ∘ g = G ∘ M ∧ g ⁡ 0 = P ⁡ 1 = ι g ∈ II Cn C | F ∘ g = G ∘ N ∧ g ⁡ 0 = P ⁡ 1

Proof

Step Hyp Ref Expression
1 cvmlift3.b ⊢ B = ⋃ C
2 cvmlift3.y ⊢ Y = ⋃ K
3 cvmlift3.f ⊢ φ → F ∈ C CovMap J
4 cvmlift3.k ⊢ φ → K ∈ SConn
5 cvmlift3.l ⊢ φ → K ∈ N-Locally PConn
6 cvmlift3.o ⊢ φ → O ∈ Y
7 cvmlift3.g ⊢ φ → G ∈ K Cn J
8 cvmlift3.p ⊢ φ → P ∈ B
9 cvmlift3.e ⊢ φ → F ⁡ P = G ⁡ O
10 cvmlift3lem1.1 ⊢ φ → M ∈ II Cn K
11 cvmlift3lem1.2 ⊢ φ → M ⁡ 0 = O
12 cvmlift3lem1.3 ⊢ φ → N ∈ II Cn K
13 cvmlift3lem1.4 ⊢ φ → N ⁡ 0 = O
14 cvmlift3lem1.5 ⊢ φ → M ⁡ 1 = N ⁡ 1
15 eqid ⊢ ι g ∈ II Cn C | F ∘ g = G ∘ M ∧ g ⁡ 0 = P = ι g ∈ II Cn C | F ∘ g = G ∘ M ∧ g ⁡ 0 = P
16 eqid ⊢ ι g ∈ II Cn C | F ∘ g = G ∘ N ∧ g ⁡ 0 = P = ι g ∈ II Cn C | F ∘ g = G ∘ N ∧ g ⁡ 0 = P
17 11 fveq2d ⊢ φ → G ⁡ M ⁡ 0 = G ⁡ O
18 9 17 eqtr4d ⊢ φ → F ⁡ P = G ⁡ M ⁡ 0
19 iiuni ⊢ 0 1 = ⋃ II
20 19 2 cnf ⊢ M ∈ II Cn K → M : 0 1 ⟶ Y
21 10 20 syl ⊢ φ → M : 0 1 ⟶ Y
22 0elunit ⊢ 0 ∈ 0 1
23 fvco3 ⊢ M : 0 1 ⟶ Y ∧ 0 ∈ 0 1 → G ∘ M ⁡ 0 = G ⁡ M ⁡ 0
24 21 22 23 sylancl ⊢ φ → G ∘ M ⁡ 0 = G ⁡ M ⁡ 0
25 18 24 eqtr4d ⊢ φ → F ⁡ P = G ∘ M ⁡ 0
26 11 13 eqtr4d ⊢ φ → M ⁡ 0 = N ⁡ 0
27 4 10 12 26 14 sconnpht2 ⊢ φ → M ≃ ph ⁡ K N
28 27 7 phtpcco2 ⊢ φ → G ∘ M ≃ ph ⁡ J G ∘ N
29 1 15 16 3 8 25 28 cvmliftpht ⊢ φ → ι g ∈ II Cn C | F ∘ g = G ∘ M ∧ g ⁡ 0 = P ≃ ph ⁡ C ι g ∈ II Cn C | F ∘ g = G ∘ N ∧ g ⁡ 0 = P
30 phtpc01 ⊢ ι g ∈ II Cn C | F ∘ g = G ∘ M ∧ g ⁡ 0 = P ≃ ph ⁡ C ι g ∈ II Cn C | F ∘ g = G ∘ N ∧ g ⁡ 0 = P → ι g ∈ II Cn C | F ∘ g = G ∘ M ∧ g ⁡ 0 = P ⁡ 0 = ι g ∈ II Cn C | F ∘ g = G ∘ N ∧ g ⁡ 0 = P ⁡ 0 ∧ ι g ∈ II Cn C | F ∘ g = G ∘ M ∧ g ⁡ 0 = P ⁡ 1 = ι g ∈ II Cn C | F ∘ g = G ∘ N ∧ g ⁡ 0 = P ⁡ 1
31 29 30 syl ⊢ φ → ι g ∈ II Cn C | F ∘ g = G ∘ M ∧ g ⁡ 0 = P ⁡ 0 = ι g ∈ II Cn C | F ∘ g = G ∘ N ∧ g ⁡ 0 = P ⁡ 0 ∧ ι g ∈ II Cn C | F ∘ g = G ∘ M ∧ g ⁡ 0 = P ⁡ 1 = ι g ∈ II Cn C | F ∘ g = G ∘ N ∧ g ⁡ 0 = P ⁡ 1
32 31 simprd ⊢ φ → ι g ∈ II Cn C | F ∘ g = G ∘ M ∧ g ⁡ 0 = P ⁡ 1 = ι g ∈ II Cn C | F ∘ g = G ∘ N ∧ g ⁡ 0 = P ⁡ 1