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 ∈ C CovMap J
cvmlift2.g ⊢ φ → G ∈ II × t II Cn J
cvmlift2.p ⊢ φ → P ∈ B
cvmlift2.i ⊢ φ → F ⁡ P = 0 G 0
cvmlift2.h ⊢ H = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ z G 0 ∧ f ⁡ 0 = P
cvmlift2.k ⊢ K = x ∈ 0 1 , y ∈ 0 1 ⟼ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y
Assertion cvmlift2lem4 ⊢ X ∈ 0 1 ∧ Y ∈ 0 1 → X K Y = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ Y

Proof

Step Hyp Ref Expression
1 cvmlift2.b ⊢ B = ⋃ C
2 cvmlift2.f ⊢ φ → F ∈ C CovMap J
3 cvmlift2.g ⊢ φ → G ∈ II × t II Cn J
4 cvmlift2.p ⊢ φ → P ∈ B
5 cvmlift2.i ⊢ φ → F ⁡ P = 0 G 0
6 cvmlift2.h ⊢ H = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ z G 0 ∧ f ⁡ 0 = P
7 cvmlift2.k ⊢ K = x ∈ 0 1 , y ∈ 0 1 ⟼ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y
8 oveq1 ⊢ x = X → x G z = X G z
9 8 mpteq2dv ⊢ x = X → z ∈ 0 1 ⟼ x G z = z ∈ 0 1 ⟼ X G z
10 9 eqeq2d ⊢ x = X → F ∘ f = z ∈ 0 1 ⟼ x G z ↔ F ∘ f = z ∈ 0 1 ⟼ X G z
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 ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ↔ F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X
14 13 riotabidv ⊢ x = X → ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X
15 14 fveq1d ⊢ x = X → ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ y
16 fveq2 ⊢ y = Y → ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ y = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ Y
17 fvex ⊢ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ Y ∈ V
18 15 16 7 17 ovmpo ⊢ X ∈ 0 1 ∧ Y ∈ 0 1 → X K Y = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ Y