Theorem cvmlift2lem2

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-2015)

	Ref	Expression
Hypotheses	cvmlift2.b	|- B = U. C
	cvmlift2.f	|- ( ph -> F e. ( C CovMap J ) )
	cvmlift2.g	|- ( ph -> G e. ( ( II tX II ) Cn J ) )
	cvmlift2.p	|- ( ph -> P e. B )
	cvmlift2.i	|- ( ph -> ( F ` P ) = ( 0 G 0 ) )
	cvmlift2.h	|- H = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( f ` 0 ) = P ) )
Assertion	cvmlift2lem2	|- ( ph -> ( H e. ( II Cn C ) /\ ( F o. H ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( H ` 0 ) = P ) )

Proof

Step	Hyp	Ref	Expression
1		cvmlift2.b	|- B = U. C
2		cvmlift2.f	|- ( ph -> F e. ( C CovMap J ) )
3		cvmlift2.g	|- ( ph -> G e. ( ( II tX II ) Cn J ) )
4		cvmlift2.p	|- ( ph -> P e. B )
5		cvmlift2.i	|- ( ph -> ( F ` P ) = ( 0 G 0 ) )
6		cvmlift2.h	|- H = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( f ` 0 ) = P ) )
7		iitopon	|- II e. ( TopOn ` ( 0 [,] 1 ) )
8	7	a1i	|- ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
9	8	cnmptid	|- ( ph -> ( z e. ( 0 [,] 1 ) |-> z ) e. ( II Cn II ) )
10		0elunit	|- 0 e. ( 0 [,] 1 )
11	10	a1i	|- ( ph -> 0 e. ( 0 [,] 1 ) )
12	8 8 11	cnmptc	|- ( ph -> ( z e. ( 0 [,] 1 ) |-> 0 ) e. ( II Cn II ) )
13	8 9 12 3	cnmpt12f	|- ( ph -> ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) e. ( II Cn J ) )
14		oveq1	|- ( z = 0 -> ( z G 0 ) = ( 0 G 0 ) )
15		eqid	|- ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) )
16		ovex	|- ( 0 G 0 ) e. _V
17	14 15 16	fvmpt	|- ( 0 e. ( 0 [,] 1 ) -> ( ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) ` 0 ) = ( 0 G 0 ) )
18	10 17	ax-mp	|- ( ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) ` 0 ) = ( 0 G 0 )
19	5 18	eqtr4di	|- ( ph -> ( F ` P ) = ( ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) ` 0 ) )
20	1 6 2 13 4 19	cvmliftiota	|- ( ph -> ( H e. ( II Cn C ) /\ ( F o. H ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( H ` 0 ) = P ) )