cvmlift2lem2

	Ref	Expression
Hypotheses	cvmlift2.b	$⊢ B = ⋃ C$
	cvmlift2.f	$⊢ φ \to F \in (C CovMap J)$
	cvmlift2.g	$⊢ φ \to G \in ((II \times_{t} II) Cn J)$
	cvmlift2.p	$⊢ φ \to P \in B$
	cvmlift2.i	$⊢ φ \to F (P) = 0 G 0$
	cvmlift2.h	$⊢ H = (ι f \in (II Cn C) \| (F \circ f = (z \in [0, 1] ⟼ z G 0) \land f (0) = P))$
Assertion	cvmlift2lem2	$⊢ φ \to (H \in (II Cn C) \land F \circ H = (z \in [0, 1] ⟼ z G 0) \land H (0) = P)$

Step	Hyp	Ref	Expression
1		cvmlift2.b	$⊢ B = ⋃ C$
2		cvmlift2.f	$⊢ φ \to F \in (C CovMap J)$
3		cvmlift2.g	$⊢ φ \to G \in ((II \times_{t} II) Cn J)$
4		cvmlift2.p	$⊢ φ \to P \in B$
5		cvmlift2.i	$⊢ φ \to F (P) = 0 G 0$
6		cvmlift2.h	$⊢ H = (ι f \in (II Cn C) \| (F \circ f = (z \in [0, 1] ⟼ z G 0) \land f (0) = P))$
7		iitopon	$⊢ II \in TopOn ([0, 1])$
8	7	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
9	8	cnmptid	$⊢ φ \to (z \in [0, 1] ⟼ z) \in (II Cn II)$
10		0elunit	$⊢ 0 \in [0, 1]$
11	10	a1i	$⊢ φ \to 0 \in [0, 1]$
12	8 8 11	cnmptc	$⊢ φ \to (z \in [0, 1] ⟼ 0) \in (II Cn II)$
13	8 9 12 3	cnmpt12f	$⊢ φ \to (z \in [0, 1] ⟼ z G 0) \in (II Cn J)$
14		oveq1	$⊢ z = 0 \to z G 0 = 0 G 0$
15		eqid	$⊢ (z \in [0, 1] ⟼ z G 0) = (z \in [0, 1] ⟼ z G 0)$
16		ovex	$⊢ 0 G 0 \in V$
17	14 15 16	fvmpt	$⊢ 0 \in [0, 1] \to (z \in [0, 1] ⟼ z G 0) (0) = 0 G 0$
18	10 17	ax-mp	$⊢ (z \in [0, 1] ⟼ z G 0) (0) = 0 G 0$
19	5 18	eqtr4di	$⊢ φ \to F (P) = (z \in [0, 1] ⟼ z G 0) (0)$
20	1 6 2 13 4 19	cvmliftiota	$⊢ φ \to (H \in (II Cn C) \land F \circ H = (z \in [0, 1] ⟼ z G 0) \land H (0) = P)$

Metamath Proof Explorer