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)

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

Proof

Step Hyp Ref Expression
1 fvmptopab.1 
 |-  ( ( ph /\ z = Z ) -> ( ch <-> ps ) )
2 fvmptopab.2 
 |-  ( ph -> { <. x , y >. | x ( F ` Z ) y } e. _V )
3 fvmptopab.3 
 |-  M = ( z e. _V |-> { <. x , y >. | ( x ( F ` z ) y /\ ch ) } )
4 fveq2 
 |-  ( z = Z -> ( F ` z ) = ( F ` Z ) )
5 4 breqd 
 |-  ( z = Z -> ( x ( F ` z ) y <-> x ( F ` Z ) y ) )
6 5 adantl 
 |-  ( ( ( Z e. _V /\ ph ) /\ z = Z ) -> ( x ( F ` z ) y <-> x ( F ` Z ) y ) )
7 1 adantll 
 |-  ( ( ( Z e. _V /\ ph ) /\ z = Z ) -> ( ch <-> ps ) )
8 6 7 anbi12d 
 |-  ( ( ( Z e. _V /\ ph ) /\ z = Z ) -> ( ( x ( F ` z ) y /\ ch ) <-> ( x ( F ` Z ) y /\ ps ) ) )
9 8 opabbidv 
 |-  ( ( ( Z e. _V /\ ph ) /\ z = Z ) -> { <. x , y >. | ( x ( F ` z ) y /\ ch ) } = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } )
10 simpl 
 |-  ( ( Z e. _V /\ ph ) -> Z e. _V )
11 id 
 |-  ( x ( F ` Z ) y -> x ( F ` Z ) y )
12 11 gen2 
 |-  A. x A. y ( x ( F ` Z ) y -> x ( F ` Z ) y )
13 2 adantl 
 |-  ( ( Z e. _V /\ ph ) -> { <. x , y >. | x ( F ` Z ) y } e. _V )
14 opabbrex 
 |-  ( ( A. x A. y ( x ( F ` Z ) y -> x ( F ` Z ) y ) /\ { <. x , y >. | x ( F ` Z ) y } e. _V ) -> { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } e. _V )
15 12 13 14 sylancr 
 |-  ( ( Z e. _V /\ ph ) -> { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } e. _V )
16 3 9 10 15 fvmptd2 
 |-  ( ( Z e. _V /\ ph ) -> ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } )
17 16 ex 
 |-  ( Z e. _V -> ( ph -> ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } ) )
18 fvprc 
 |-  ( -. Z e. _V -> ( M ` Z ) = (/) )
19 br0 
 |-  -. x (/) y
20 fvprc 
 |-  ( -. Z e. _V -> ( F ` Z ) = (/) )
21 20 breqd 
 |-  ( -. Z e. _V -> ( x ( F ` Z ) y <-> x (/) y ) )
22 19 21 mtbiri 
 |-  ( -. Z e. _V -> -. x ( F ` Z ) y )
23 22 intnanrd 
 |-  ( -. Z e. _V -> -. ( x ( F ` Z ) y /\ ps ) )
24 23 alrimivv 
 |-  ( -. Z e. _V -> A. x A. y -. ( x ( F ` Z ) y /\ ps ) )
25 opab0 
 |-  ( { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } = (/) <-> A. x A. y -. ( x ( F ` Z ) y /\ ps ) )
26 24 25 sylibr 
 |-  ( -. Z e. _V -> { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } = (/) )
27 18 26 eqtr4d 
 |-  ( -. Z e. _V -> ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } )
28 27 a1d 
 |-  ( -. Z e. _V -> ( ph -> ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } ) )
29 17 28 pm2.61i 
 |-  ( ph -> ( M ` Z ) = { <. x , y >. | ( x ( F ` Z ) y /\ ps ) } )