Metamath Proof Explorer

Theorem cvmlift2lem6

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 cvmlift2lem6 ⊢φ∧X∈01→K↾X×01∈II×tII↾𝑡X×01CnC

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 1 2 3 4 5 6 7 cvmlift2lem5 ⊢φ→K:01×01⟶B
9 8 adantr ⊢φ∧X∈01→K:01×01⟶B
10 9 ffnd ⊢φ∧X∈01→KFn01×01
11 fnov ⊢KFn01×01↔K=u∈01,v∈01⟼uKv
12 10 11 sylib ⊢φ∧X∈01→K=u∈01,v∈01⟼uKv
13 12 reseq1d ⊢φ∧X∈01→K↾X×01=u∈01,v∈01⟼uKv↾X×01
14 simpr ⊢φ∧X∈01→X∈01
15 14 snssd ⊢φ∧X∈01→X⊆01
16 ssid ⊢01⊆01
17 resmpo ⊢X⊆01∧01⊆01→u∈01,v∈01⟼uKv↾X×01=u∈X,v∈01⟼uKv
18 15 16 17 sylancl ⊢φ∧X∈01→u∈01,v∈01⟼uKv↾X×01=u∈X,v∈01⟼uKv
19 elsni ⊢u∈X→u=X
20 19 3ad2ant2 ⊢φ∧X∈01∧u∈X∧v∈01→u=X
21 20 oveq1d ⊢φ∧X∈01∧u∈X∧v∈01→uKv=XKv
22 simp1r ⊢φ∧X∈01∧u∈X∧v∈01→X∈01
23 simp3 ⊢φ∧X∈01∧u∈X∧v∈01→v∈01
24 1 2 3 4 5 6 7 cvmlift2lem4 ⊢X∈01∧v∈01→XKv=ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡v
25 22 23 24 syl2anc ⊢φ∧X∈01∧u∈X∧v∈01→XKv=ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡v
26 21 25 eqtrd ⊢φ∧X∈01∧u∈X∧v∈01→uKv=ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡v
27 26 mpoeq3dva ⊢φ∧X∈01→u∈X,v∈01⟼uKv=u∈X,v∈01⟼ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡v
28 18 27 eqtrd ⊢φ∧X∈01→u∈01,v∈01⟼uKv↾X×01=u∈X,v∈01⟼ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡v
29 13 28 eqtrd ⊢φ∧X∈01→K↾X×01=u∈X,v∈01⟼ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡v
30 eqid ⊢II↾𝑡X=II↾𝑡X
31 iitopon ⊢II∈TopOn⁡01
32 31 a1i ⊢φ∧X∈01→II∈TopOn⁡01
33 eqid ⊢II↾𝑡01=II↾𝑡01
34 16 a1i ⊢φ∧X∈01→01⊆01
35 32 32 cnmpt2nd ⊢φ∧X∈01→u∈01,v∈01⟼v∈II×tIICnII
36 eqid ⊢ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X=ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X
37 1 2 3 4 5 6 36 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
38 37 simp1d ⊢φ∧X∈01→ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X∈IICnC
39 32 32 35 38 cnmpt21f ⊢φ∧X∈01→u∈01,v∈01⟼ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡v∈II×tIICnC
40 30 32 15 33 32 34 39 cnmpt2res ⊢φ∧X∈01→u∈X,v∈01⟼ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡v∈II↾𝑡X×tII↾𝑡01CnC
41 iitop ⊢II∈Top
42 snex ⊢X∈V
43 ovex ⊢01∈V
44 txrest ⊢II∈Top∧II∈Top∧X∈V∧01∈V→II×tII↾𝑡X×01=II↾𝑡X×tII↾𝑡01
45 41 41 42 43 44 mp4an ⊢II×tII↾𝑡X×01=II↾𝑡X×tII↾𝑡01
46 45 oveq1i ⊢II×tII↾𝑡X×01CnC=II↾𝑡X×tII↾𝑡01CnC
47 40 46 eleqtrrdi ⊢φ∧X∈01→u∈X,v∈01⟼ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡v∈II×tII↾𝑡X×01CnC
48 29 47 eqeltrd ⊢φ∧X∈01→K↾X×01∈II×tII↾𝑡X×01CnC