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 syl6eqr φ 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