Metamath Proof Explorer

Theorem cvmlift2lem4

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 1-Jun-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 ) )
		cvmlift2.k	\|- K = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) \|-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) )
	Assertion	cvmlift2lem4	\|- ( ( X e. ( 0 [,] 1 ) /\ Y e. ( 0 [,] 1 ) ) -> ( X K Y ) = ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` Y ) )

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		cvmlift2.k	\|- K = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) \|-> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) )
8		oveq1	\|- ( x = X -> ( x G z ) = ( X G z ) )
9	8	mpteq2dv	\|- ( x = X -> ( z e. ( 0 [,] 1 ) \|-> ( x G z ) ) = ( z e. ( 0 [,] 1 ) \|-> ( X G z ) ) )
10	9	eqeq2d	\|- ( x = X -> ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( x G z ) ) <-> ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( X G z ) ) ) )
11		fveq2	\|- ( x = X -> ( H ` x ) = ( H ` X ) )
12	11	eqeq2d	\|- ( x = X -> ( ( f ` 0 ) = ( H ` x ) <-> ( f ` 0 ) = ( H ` X ) ) )
13	10 12	anbi12d	\|- ( x = X -> ( ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) <-> ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) )
14	13	riotabidv	\|- ( x = X -> ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) )
15	14	fveq1d	\|- ( x = X -> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( x G z ) ) /\ ( f ` 0 ) = ( H ` x ) ) ) ` y ) = ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` y ) )
16		fveq2	\|- ( y = Y -> ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` y ) = ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` Y ) )
17		fvex	\|- ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` Y ) e. _V
18	15 16 7 17	ovmpo	\|- ( ( X e. ( 0 [,] 1 ) /\ Y e. ( 0 [,] 1 ) ) -> ( X K Y ) = ( ( iota_ f e. ( II Cn C ) ( ( F o. f ) = ( z e. ( 0 [,] 1 ) \|-> ( X G z ) ) /\ ( f ` 0 ) = ( H ` X ) ) ) ` Y ) )