Metamath Proof Explorer

Theorem cvmlift2lem7

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
cvmlift2.k ⊢K=x∈01,y∈01⟼ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y
Assertion cvmlift2lem7 ⊢φ→F∘K=G

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 cvmlift2.k ⊢K=x∈01,y∈01⟼ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y
8 eqid ⊢ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x=ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x
9 1 2 3 4 5 6 8 cvmlift2lem3 ⊢φ∧x∈01→ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x∈IICnC∧F∘ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x=z∈01⟼xGz∧ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡0=H⁡x
10 9 adantrr ⊢φ∧x∈01∧y∈01→ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x∈IICnC∧F∘ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x=z∈01⟼xGz∧ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡0=H⁡x
11 10 simp2d ⊢φ∧x∈01∧y∈01→F∘ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x=z∈01⟼xGz
12 11 fveq1d ⊢φ∧x∈01∧y∈01→F∘ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y=z∈01⟼xGz⁡y
13 10 simp1d ⊢φ∧x∈01∧y∈01→ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x∈IICnC
14 iiuni ⊢01=⋃II
15 14 1 cnf ⊢ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x∈IICnC→ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x:01⟶B
16 13 15 syl ⊢φ∧x∈01∧y∈01→ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x:01⟶B
17 simprr ⊢φ∧x∈01∧y∈01→y∈01
18 fvco3 ⊢ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x:01⟶B∧y∈01→F∘ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y=F⁡ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y
19 16 17 18 syl2anc ⊢φ∧x∈01∧y∈01→F∘ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y=F⁡ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y
20 oveq2 ⊢z=y→xGz=xGy
21 eqid ⊢z∈01⟼xGz=z∈01⟼xGz
22 ovex ⊢xGy∈V
23 20 21 22 fvmpt ⊢y∈01→z∈01⟼xGz⁡y=xGy
24 17 23 syl ⊢φ∧x∈01∧y∈01→z∈01⟼xGz⁡y=xGy
25 12 19 24 3eqtr3d ⊢φ∧x∈01∧y∈01→F⁡ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y=xGy
26 25 3impb ⊢φ∧x∈01∧y∈01→F⁡ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y=xGy
27 26 mpoeq3dva ⊢φ→x∈01,y∈01⟼F⁡ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y=x∈01,y∈01⟼xGy
28 16 17 ffvelcdmd ⊢φ∧x∈01∧y∈01→ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y∈B
29 7 a1i ⊢φ→K=x∈01,y∈01⟼ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y
30 cvmcn ⊢F∈CCovMapJ→F∈CCnJ
31 eqid ⊢⋃J=⋃J
32 1 31 cnf ⊢F∈CCnJ→F:B⟶⋃J
33 2 30 32 3syl ⊢φ→F:B⟶⋃J
34 33 feqmptd ⊢φ→F=w∈B⟼F⁡w
35 fveq2 ⊢w=ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y→F⁡w=F⁡ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y
36 28 29 34 35 fmpoco ⊢φ→F∘K=x∈01,y∈01⟼F⁡ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y
37 iitop ⊢II∈Top
38 37 37 14 14 txunii ⊢01×01=⋃II×tII
39 38 31 cnf ⊢G∈II×tIICnJ→G:01×01⟶⋃J
40 ffn ⊢G:01×01⟶⋃J→GFn01×01
41 3 39 40 3syl ⊢φ→GFn01×01
42 fnov ⊢GFn01×01↔G=x∈01,y∈01⟼xGy
43 41 42 sylib ⊢φ→G=x∈01,y∈01⟼xGy
44 27 36 43 3eqtr4d ⊢φ→F∘K=G