Metamath Proof Explorer

Theorem cvmlift2lem5

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 cvmlift2lem5 ⊢φ→K:01×01⟶B

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 simp1d ⊢φ∧x∈01∧y∈01→ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x∈IICnC
12 iiuni ⊢01=⋃II
13 12 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
14 11 13 syl ⊢φ∧x∈01∧y∈01→ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x:01⟶B
15 simprr ⊢φ∧x∈01∧y∈01→y∈01
16 14 15 ffvelcdmd ⊢φ∧x∈01∧y∈01→ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y∈B
17 16 ralrimivva ⊢φ→∀x∈01∀y∈01ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y∈B
18 7 fmpo ⊢∀x∈01∀y∈01ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y∈B↔K:01×01⟶B
19 17 18 sylib ⊢φ→K:01×01⟶B