Metamath Proof Explorer

Theorem cvmlift3lem5

Description: Lemma for cvmlift2 . (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
cvmlift3.h ⊢ H = x ∈ Y ⟼ ι z ∈ B | ∃ f ∈ II Cn K f ⁡ 0 = O ∧ f ⁡ 1 = x ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = z
Assertion cvmlift3lem5 ⊢ φ → F ∘ H = G

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 cvmlift3.h ⊢ H = x ∈ Y ⟼ ι z ∈ B | ∃ f ∈ II Cn K f ⁡ 0 = O ∧ f ⁡ 1 = x ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = z
11 eqid ⊢ H ⁡ y = H ⁡ y
12 1 2 3 4 5 6 7 8 9 10 cvmlift3lem4 ⊢ φ ∧ y ∈ Y → H ⁡ y = H ⁡ y ↔ ∃ f ∈ II Cn K f ⁡ 0 = O ∧ f ⁡ 1 = y ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = H ⁡ y
13 11 12 mpbii ⊢ φ ∧ y ∈ Y → ∃ f ∈ II Cn K f ⁡ 0 = O ∧ f ⁡ 1 = y ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = H ⁡ y
14 df-3an ⊢ f ⁡ 0 = O ∧ f ⁡ 1 = y ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = H ⁡ y ↔ f ⁡ 0 = O ∧ f ⁡ 1 = y ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = H ⁡ y
15 eqid ⊢ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P = ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P
16 3 ad3antrrr ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → F ∈ C CovMap J
17 simplr ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → f ∈ II Cn K
18 7 ad3antrrr ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → G ∈ K Cn J
19 cnco ⊢ f ∈ II Cn K ∧ G ∈ K Cn J → G ∘ f ∈ II Cn J
20 17 18 19 syl2anc ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → G ∘ f ∈ II Cn J
21 8 ad3antrrr ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → P ∈ B
22 simprl ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → f ⁡ 0 = O
23 22 fveq2d ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → G ⁡ f ⁡ 0 = G ⁡ O
24 iiuni ⊢ 0 1 = ⋃ II
25 24 2 cnf ⊢ f ∈ II Cn K → f : 0 1 ⟶ Y
26 17 25 syl ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → f : 0 1 ⟶ Y
27 0elunit ⊢ 0 ∈ 0 1
28 fvco3 ⊢ f : 0 1 ⟶ Y ∧ 0 ∈ 0 1 → G ∘ f ⁡ 0 = G ⁡ f ⁡ 0
29 26 27 28 sylancl ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → G ∘ f ⁡ 0 = G ⁡ f ⁡ 0
30 9 ad3antrrr ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → F ⁡ P = G ⁡ O
31 23 29 30 3eqtr4rd ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → F ⁡ P = G ∘ f ⁡ 0
32 1 15 16 20 21 31 cvmliftiota ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ∈ II Cn C ∧ F ∘ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P = G ∘ f ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 0 = P
33 32 simp2d ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → F ∘ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P = G ∘ f
34 33 fveq1d ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → F ∘ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = G ∘ f ⁡ 1
35 32 simp1d ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ∈ II Cn C
36 24 1 cnf ⊢ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ∈ II Cn C → ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P : 0 1 ⟶ B
37 35 36 syl ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P : 0 1 ⟶ B
38 1elunit ⊢ 1 ∈ 0 1
39 fvco3 ⊢ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P : 0 1 ⟶ B ∧ 1 ∈ 0 1 → F ∘ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = F ⁡ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1
40 37 38 39 sylancl ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → F ∘ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = F ⁡ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1
41 fvco3 ⊢ f : 0 1 ⟶ Y ∧ 1 ∈ 0 1 → G ∘ f ⁡ 1 = G ⁡ f ⁡ 1
42 26 38 41 sylancl ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → G ∘ f ⁡ 1 = G ⁡ f ⁡ 1
43 simprr ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → f ⁡ 1 = y
44 43 fveq2d ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → G ⁡ f ⁡ 1 = G ⁡ y
45 42 44 eqtrd ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → G ∘ f ⁡ 1 = G ⁡ y
46 34 40 45 3eqtr3d ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → F ⁡ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = G ⁡ y
47 fveqeq2 ⊢ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = H ⁡ y → F ⁡ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = G ⁡ y ↔ F ⁡ H ⁡ y = G ⁡ y
48 46 47 syl5ibcom ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K ∧ f ⁡ 0 = O ∧ f ⁡ 1 = y → ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = H ⁡ y → F ⁡ H ⁡ y = G ⁡ y
49 48 expimpd ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K → f ⁡ 0 = O ∧ f ⁡ 1 = y ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = H ⁡ y → F ⁡ H ⁡ y = G ⁡ y
50 14 49 syl5bi ⊢ φ ∧ y ∈ Y ∧ f ∈ II Cn K → f ⁡ 0 = O ∧ f ⁡ 1 = y ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = H ⁡ y → F ⁡ H ⁡ y = G ⁡ y
51 50 rexlimdva ⊢ φ ∧ y ∈ Y → ∃ f ∈ II Cn K f ⁡ 0 = O ∧ f ⁡ 1 = y ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = H ⁡ y → F ⁡ H ⁡ y = G ⁡ y
52 13 51 mpd ⊢ φ ∧ y ∈ Y → F ⁡ H ⁡ y = G ⁡ y
53 52 mpteq2dva ⊢ φ → y ∈ Y ⟼ F ⁡ H ⁡ y = y ∈ Y ⟼ G ⁡ y
54 1 2 3 4 5 6 7 8 9 10 cvmlift3lem3 ⊢ φ → H : Y ⟶ B
55 54 ffvelrnda ⊢ φ ∧ y ∈ Y → H ⁡ y ∈ B
56 54 feqmptd ⊢ φ → H = y ∈ Y ⟼ H ⁡ y
57 cvmcn ⊢ F ∈ C CovMap J → F ∈ C Cn J
58 eqid ⊢ ⋃ J = ⋃ J
59 1 58 cnf ⊢ F ∈ C Cn J → F : B ⟶ ⋃ J
60 3 57 59 3syl ⊢ φ → F : B ⟶ ⋃ J
61 60 feqmptd ⊢ φ → F = w ∈ B ⟼ F ⁡ w
62 fveq2 ⊢ w = H ⁡ y → F ⁡ w = F ⁡ H ⁡ y
63 55 56 61 62 fmptco ⊢ φ → F ∘ H = y ∈ Y ⟼ F ⁡ H ⁡ y
64 2 58 cnf ⊢ G ∈ K Cn J → G : Y ⟶ ⋃ J
65 7 64 syl ⊢ φ → G : Y ⟶ ⋃ J
66 65 feqmptd ⊢ φ → G = y ∈ Y ⟼ G ⁡ y
67 53 63 66 3eqtr4d ⊢ φ → F ∘ H = G