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∈CCovMapJ
cvmlift3.k ⊢φ→K∈SConn
cvmlift3.l ⊢φ→K∈N-Locally PConn
cvmlift3.o ⊢φ→O∈Y
cvmlift3.g ⊢φ→G∈KCnJ
cvmlift3.p ⊢φ→P∈B
cvmlift3.e ⊢φ→F⁡P=G⁡O
cvmlift3.h ⊢H=x∈Y⟼ιz∈B|∃f∈IICnKf⁡0=O∧f⁡1=x∧ιg∈IICnC|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∈CCovMapJ
4 cvmlift3.k ⊢φ→K∈SConn
5 cvmlift3.l ⊢φ→K∈N-Locally PConn
6 cvmlift3.o ⊢φ→O∈Y
7 cvmlift3.g ⊢φ→G∈KCnJ
8 cvmlift3.p ⊢φ→P∈B
9 cvmlift3.e ⊢φ→F⁡P=G⁡O
10 cvmlift3.h ⊢H=x∈Y⟼ιz∈B|∃f∈IICnKf⁡0=O∧f⁡1=x∧ιg∈IICnC|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∈IICnKf⁡0=O∧f⁡1=y∧ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=H⁡y
13 11 12 mpbii ⊢φ∧y∈Y→∃f∈IICnKf⁡0=O∧f⁡1=y∧ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=H⁡y
14 df-3an ⊢f⁡0=O∧f⁡1=y∧ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=H⁡y↔f⁡0=O∧f⁡1=y∧ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=H⁡y
15 eqid ⊢ιg∈IICnC|F∘g=G∘f∧g⁡0=P=ιg∈IICnC|F∘g=G∘f∧g⁡0=P
16 3 ad3antrrr ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→F∈CCovMapJ
17 simplr ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→f∈IICnK
18 7 ad3antrrr ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→G∈KCnJ
19 cnco ⊢f∈IICnK∧G∈KCnJ→G∘f∈IICnJ
20 17 18 19 syl2anc ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→G∘f∈IICnJ
21 8 ad3antrrr ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→P∈B
22 simprl ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→f⁡0=O
23 22 fveq2d ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→G⁡f⁡0=G⁡O
24 iiuni ⊢01=⋃II
25 24 2 cnf ⊢f∈IICnK→f:01⟶Y
26 17 25 syl ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→f:01⟶Y
27 0elunit ⊢0∈01
28 fvco3 ⊢f:01⟶Y∧0∈01→G∘f⁡0=G⁡f⁡0
29 26 27 28 sylancl ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→G∘f⁡0=G⁡f⁡0
30 9 ad3antrrr ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→F⁡P=G⁡O
31 23 29 30 3eqtr4rd ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→F⁡P=G∘f⁡0
32 1 15 16 20 21 31 cvmliftiota ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→ιg∈IICnC|F∘g=G∘f∧g⁡0=P∈IICnC∧F∘ιg∈IICnC|F∘g=G∘f∧g⁡0=P=G∘f∧ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡0=P
33 32 simp2d ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→F∘ιg∈IICnC|F∘g=G∘f∧g⁡0=P=G∘f
34 33 fveq1d ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→F∘ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=G∘f⁡1
35 32 simp1d ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→ιg∈IICnC|F∘g=G∘f∧g⁡0=P∈IICnC
36 24 1 cnf ⊢ιg∈IICnC|F∘g=G∘f∧g⁡0=P∈IICnC→ιg∈IICnC|F∘g=G∘f∧g⁡0=P:01⟶B
37 35 36 syl ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→ιg∈IICnC|F∘g=G∘f∧g⁡0=P:01⟶B
38 1elunit ⊢1∈01
39 fvco3 ⊢ιg∈IICnC|F∘g=G∘f∧g⁡0=P:01⟶B∧1∈01→F∘ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=F⁡ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1
40 37 38 39 sylancl ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→F∘ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=F⁡ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1
41 fvco3 ⊢f:01⟶Y∧1∈01→G∘f⁡1=G⁡f⁡1
42 26 38 41 sylancl ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→G∘f⁡1=G⁡f⁡1
43 simprr ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→f⁡1=y
44 43 fveq2d ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→G⁡f⁡1=G⁡y
45 42 44 eqtrd ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→G∘f⁡1=G⁡y
46 34 40 45 3eqtr3d ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→F⁡ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=G⁡y
47 fveqeq2 ⊢ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=H⁡y→F⁡ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=G⁡y↔F⁡H⁡y=G⁡y
48 46 47 syl5ibcom ⊢φ∧y∈Y∧f∈IICnK∧f⁡0=O∧f⁡1=y→ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=H⁡y→F⁡H⁡y=G⁡y
49 48 expimpd ⊢φ∧y∈Y∧f∈IICnK→f⁡0=O∧f⁡1=y∧ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=H⁡y→F⁡H⁡y=G⁡y
50 14 49 biimtrid ⊢φ∧y∈Y∧f∈IICnK→f⁡0=O∧f⁡1=y∧ιg∈IICnC|F∘g=G∘f∧g⁡0=P⁡1=H⁡y→F⁡H⁡y=G⁡y
51 50 rexlimdva ⊢φ∧y∈Y→∃f∈IICnKf⁡0=O∧f⁡1=y∧ιg∈IICnC|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 ffvelcdmda ⊢φ∧y∈Y→H⁡y∈B
56 54 feqmptd ⊢φ→H=y∈Y⟼H⁡y
57 cvmcn ⊢F∈CCovMapJ→F∈CCnJ
58 eqid ⊢⋃J=⋃J
59 1 58 cnf ⊢F∈CCnJ→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∈KCnJ→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