Metamath Proof Explorer

Theorem cvmlift2lem8

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 9-Mar-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 cvmlift2lem8 ⊢ φ ∧ X ∈ 0 1 → X K 0 = H ⁡ X

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 simpr ⊢ φ ∧ X ∈ 0 1 → X ∈ 0 1
9 0elunit ⊢ 0 ∈ 0 1
10 1 2 3 4 5 6 7 cvmlift2lem4 ⊢ X ∈ 0 1 ∧ 0 ∈ 0 1 → X K 0 = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ 0
11 8 9 10 sylancl ⊢ φ ∧ X ∈ 0 1 → X K 0 = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ 0
12 eqid ⊢ ι 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
13 1 2 3 4 5 6 12 cvmlift2lem3 ⊢ φ ∧ X ∈ 0 1 → ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ∈ II Cn C ∧ F ∘ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X = z ∈ 0 1 ⟼ X G z ∧ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ 0 = H ⁡ X
14 13 simp3d ⊢ φ ∧ X ∈ 0 1 → ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ 0 = H ⁡ X
15 11 14 eqtrd ⊢ φ ∧ X ∈ 0 1 → X K 0 = H ⁡ X