Theorem sprmpod

Description: The extension of a binary relation which is the value of an operation given in maps-to notation. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 20-Jun-2019)

	Ref	Expression
Hypotheses	sprmpod.1	|- M = ( v e. _V , e e. _V |-> { <. x , y >. | ( x ( v R e ) y /\ ch ) } )
	sprmpod.2	|- ( ( ph /\ v = V /\ e = E ) -> ( ch <-> ps ) )
	sprmpod.3	|- ( ph -> ( V e. _V /\ E e. _V ) )
	sprmpod.4	|- ( ph -> A. x A. y ( x ( V R E ) y -> th ) )
	sprmpod.5	|- ( ph -> { <. x , y >. | th } e. _V )
Assertion	sprmpod	|- ( ph -> ( V M E ) = { <. x , y >. | ( x ( V R E ) y /\ ps ) } )

Proof

Step	Hyp	Ref	Expression
1		sprmpod.1	|- M = ( v e. _V , e e. _V |-> { <. x , y >. | ( x ( v R e ) y /\ ch ) } )
2		sprmpod.2	|- ( ( ph /\ v = V /\ e = E ) -> ( ch <-> ps ) )
3		sprmpod.3	|- ( ph -> ( V e. _V /\ E e. _V ) )
4		sprmpod.4	|- ( ph -> A. x A. y ( x ( V R E ) y -> th ) )
5		sprmpod.5	|- ( ph -> { <. x , y >. | th } e. _V )
6	1	a1i	|- ( ph -> M = ( v e. _V , e e. _V |-> { <. x , y >. | ( x ( v R e ) y /\ ch ) } ) )
7		oveq12	|- ( ( v = V /\ e = E ) -> ( v R e ) = ( V R E ) )
8	7	breqd	|- ( ( v = V /\ e = E ) -> ( x ( v R e ) y <-> x ( V R E ) y ) )
9	8	adantl	|- ( ( ph /\ ( v = V /\ e = E ) ) -> ( x ( v R e ) y <-> x ( V R E ) y ) )
10	2	3expb	|- ( ( ph /\ ( v = V /\ e = E ) ) -> ( ch <-> ps ) )
11	9 10	anbi12d	|- ( ( ph /\ ( v = V /\ e = E ) ) -> ( ( x ( v R e ) y /\ ch ) <-> ( x ( V R E ) y /\ ps ) ) )
12	11	opabbidv	|- ( ( ph /\ ( v = V /\ e = E ) ) -> { <. x , y >. | ( x ( v R e ) y /\ ch ) } = { <. x , y >. | ( x ( V R E ) y /\ ps ) } )
13	3	simpld	|- ( ph -> V e. _V )
14	3	simprd	|- ( ph -> E e. _V )
15		opabbrex	|- ( ( A. x A. y ( x ( V R E ) y -> th ) /\ { <. x , y >. | th } e. _V ) -> { <. x , y >. | ( x ( V R E ) y /\ ps ) } e. _V )
16	4 5 15	syl2anc	|- ( ph -> { <. x , y >. | ( x ( V R E ) y /\ ps ) } e. _V )
17	6 12 13 14 16	ovmpod	|- ( ph -> ( V M E ) = { <. x , y >. | ( x ( V R E ) y /\ ps ) } )