This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) } )