Theorem fvmptopab

Description: The function value of a mapping M to a restricted binary relation expressed as an ordered-pair class abstraction: The restricted binary relation is a binary relation given as value of a function F restricted by the condition ps . (Contributed by AV, 31-Jan-2021) (Revised by AV, 29-Oct-2021) Add disjoint variable condition on F , x , y to remove a sethood hypothesis. (Revised by SN, 13-Dec-2024)

	Ref	Expression
Hypotheses	fvmptopab.1	|- ( z = Z -> ( ph <-> ps ) )
	fvmptopab.m	|- M = ( z e. _V |-> { <. x , y >. | ( x ( F ` z ) y /\ ph ) } )
Assertion	fvmptopab	|- ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) }

Proof

Step	Hyp	Ref	Expression
1		fvmptopab.1	|- ( z = Z -> ( ph <-> ps ) )
2		fvmptopab.m	|- M = ( z e. _V |-> { <. x , y >. | ( x ( F ` z ) y /\ ph ) } )
3		fveq2	|- ( z = Z -> ( F ` z ) = ( F ` Z ) )
4	3	breqd	|- ( z = Z -> ( x ( F ` z ) y <-> x ( F ` Z ) y ) )
5	4 1	anbi12d	|- ( z = Z -> ( ( x ( F ` z ) y /\ ph ) <-> ( x ( F ` Z ) y /\ ps ) ) )
6	5	opabbidv	|- ( z = Z -> { <. x , y >. | ( x ( F ` z ) y /\ ph ) } = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } )
7		opabresex2	|- { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } e. _V
8	6 2 7	fvmpt	|- ( Z e. _V -> ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } )
9		fvprc	|- ( -. Z e. _V -> ( M ` Z ) = (/) )
10		elopabran	|- ( z e. { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } -> z e. ( F ` Z ) )
11	10	ssriv	|- { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } C_ ( F ` Z )
12		fvprc	|- ( -. Z e. _V -> ( F ` Z ) = (/) )
13	11 12	sseqtrid	|- ( -. Z e. _V -> { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } C_ (/) )
14		ss0	|- ( { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } C_ (/) -> { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } = (/) )
15	13 14	syl	|- ( -. Z e. _V -> { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } = (/) )
16	9 15	eqtr4d	|- ( -. Z e. _V -> ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } )
17	8 16	pm2.61i	|- ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) }