Metamath Proof Explorer

Theorem cvmlift2lem3

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses cvmlift2.b ⊢B=⋃C
cvmlift2.f ⊢φ→F∈CCovMapJ
cvmlift2.g ⊢φ→G∈II×tIICnJ
cvmlift2.p ⊢φ→P∈B
cvmlift2.i ⊢φ→F⁡P=0G0
cvmlift2.h ⊢H=ιf∈IICnC|F∘f=z∈01⟼zG0∧f⁡0=P
cvmlift2lem3.1 ⊢K=ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X
Assertion cvmlift2lem3 ⊢φ∧X∈01→K∈IICnC∧F∘K=z∈01⟼XGz∧K⁡0=H⁡X

Proof

Step Hyp Ref Expression
1 cvmlift2.b ⊢B=⋃C
2 cvmlift2.f ⊢φ→F∈CCovMapJ
3 cvmlift2.g ⊢φ→G∈II×tIICnJ
4 cvmlift2.p ⊢φ→P∈B
5 cvmlift2.i ⊢φ→F⁡P=0G0
6 cvmlift2.h ⊢H=ιf∈IICnC|F∘f=z∈01⟼zG0∧f⁡0=P
7 cvmlift2lem3.1 ⊢K=ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X
8 2 adantr ⊢φ∧X∈01→F∈CCovMapJ
9 iitopon ⊢II∈TopOn⁡01
10 9 a1i ⊢φ∧X∈01→II∈TopOn⁡01
11 simpr ⊢φ∧X∈01→X∈01
12 10 10 11 cnmptc ⊢φ∧X∈01→z∈01⟼X∈IICnII
13 10 cnmptid ⊢φ∧X∈01→z∈01⟼z∈IICnII
14 3 adantr ⊢φ∧X∈01→G∈II×tIICnJ
15 10 12 13 14 cnmpt12f ⊢φ∧X∈01→z∈01⟼XGz∈IICnJ
16 1 2 3 4 5 6 cvmlift2lem2 ⊢φ→H∈IICnC∧F∘H=z∈01⟼zG0∧H⁡0=P
17 16 simp1d ⊢φ→H∈IICnC
18 iiuni ⊢01=⋃II
19 18 1 cnf ⊢H∈IICnC→H:01⟶B
20 17 19 syl ⊢φ→H:01⟶B
21 20 ffvelcdmda ⊢φ∧X∈01→H⁡X∈B
22 0elunit ⊢0∈01
23 oveq2 ⊢z=0→XGz=XG0
24 eqid ⊢z∈01⟼XGz=z∈01⟼XGz
25 ovex ⊢XG0∈V
26 23 24 25 fvmpt ⊢0∈01→z∈01⟼XGz⁡0=XG0
27 22 26 mp1i ⊢φ∧X∈01→z∈01⟼XGz⁡0=XG0
28 16 simp2d ⊢φ→F∘H=z∈01⟼zG0
29 28 fveq1d ⊢φ→F∘H⁡X=z∈01⟼zG0⁡X
30 oveq1 ⊢z=X→zG0=XG0
31 eqid ⊢z∈01⟼zG0=z∈01⟼zG0
32 30 31 25 fvmpt ⊢X∈01→z∈01⟼zG0⁡X=XG0
33 29 32 sylan9eq ⊢φ∧X∈01→F∘H⁡X=XG0
34 fvco3 ⊢H:01⟶B∧X∈01→F∘H⁡X=F⁡H⁡X
35 20 34 sylan ⊢φ∧X∈01→F∘H⁡X=F⁡H⁡X
36 27 33 35 3eqtr2rd ⊢φ∧X∈01→F⁡H⁡X=z∈01⟼XGz⁡0
37 1 7 8 15 21 36 cvmliftiota ⊢φ∧X∈01→K∈IICnC∧F∘K=z∈01⟼XGz∧K⁡0=H⁡X