Metamath Proof Explorer

Theorem cvmlift2lem4

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 1-Jun-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 cvmlift2lem4 ⊢X∈01∧Y∈01→XKY=ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡Y

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 oveq1 ⊢x=X→xGz=XGz
9 8 mpteq2dv ⊢x=X→z∈01⟼xGz=z∈01⟼XGz
10 9 eqeq2d ⊢x=X→F∘f=z∈01⟼xGz↔F∘f=z∈01⟼XGz
11 fveq2 ⊢x=X→H⁡x=H⁡X
12 11 eqeq2d ⊢x=X→f⁡0=H⁡x↔f⁡0=H⁡X
13 10 12 anbi12d ⊢x=X→F∘f=z∈01⟼xGz∧f⁡0=H⁡x↔F∘f=z∈01⟼XGz∧f⁡0=H⁡X
14 13 riotabidv ⊢x=X→ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x=ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X
15 14 fveq1d ⊢x=X→ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y=ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡y
16 fveq2 ⊢y=Y→ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡y=ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡Y
17 fvex ⊢ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡Y∈V
18 15 16 7 17 ovmpo ⊢X∈01∧Y∈01→XKY=ιf∈IICnC|F∘f=z∈01⟼XGz∧f⁡0=H⁡X⁡Y