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

Metamath Proof Explorer

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