Metamath Proof Explorer

Theorem cvmlift2lem2

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-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
Assertion cvmlift2lem2 ⊢ φ → H ∈ II Cn C ∧ F ∘ H = z ∈ 0 1 ⟼ z G 0 ∧ H ⁡ 0 = P

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 iitopon ⊢ II ∈ TopOn ⁡ 0 1
8 7 a1i ⊢ φ → II ∈ TopOn ⁡ 0 1
9 8 cnmptid ⊢ φ → z ∈ 0 1 ⟼ z ∈ II Cn II
10 0elunit ⊢ 0 ∈ 0 1
11 10 a1i ⊢ φ → 0 ∈ 0 1
12 8 8 11 cnmptc ⊢ φ → z ∈ 0 1 ⟼ 0 ∈ II Cn II
13 8 9 12 3 cnmpt12f ⊢ φ → z ∈ 0 1 ⟼ z G 0 ∈ II Cn J
14 oveq1 ⊢ z = 0 → z G 0 = 0 G 0
15 eqid ⊢ z ∈ 0 1 ⟼ z G 0 = z ∈ 0 1 ⟼ z G 0
16 ovex ⊢ 0 G 0 ∈ V
17 14 15 16 fvmpt ⊢ 0 ∈ 0 1 → z ∈ 0 1 ⟼ z G 0 ⁡ 0 = 0 G 0
18 10 17 ax-mp ⊢ z ∈ 0 1 ⟼ z G 0 ⁡ 0 = 0 G 0
19 5 18 eqtr4di ⊢ φ → F ⁡ P = z ∈ 0 1 ⟼ z G 0 ⁡ 0
20 1 6 2 13 4 19 cvmliftiota ⊢ φ → H ∈ II Cn C ∧ F ∘ H = z ∈ 0 1 ⟼ z G 0 ∧ H ⁡ 0 = P