Metamath Proof Explorer

Theorem suppvalbr

Description: The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019)

Ref Expression
Assertion suppvalbr 
|- ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = { x | ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) } )

Proof

Step Hyp Ref Expression
1 df-rab 
 |-  { x e. dom R | ( R " { x } ) =/= { Z } } = { x | ( x e. dom R /\ ( R " { x } ) =/= { Z } ) }
2 vex 
 |-  x e. _V
3 2 eldm 
 |-  ( x e. dom R <-> E. y x R y )
4 imasng 
 |-  ( x e. _V -> ( R " { x } ) = { y | x R y } )
5 4 elv 
 |-  ( R " { x } ) = { y | x R y }
6 5 neeq1i 
 |-  ( ( R " { x } ) =/= { Z } <-> { y | x R y } =/= { Z } )
7 df-sn 
 |-  { Z } = { y | y = Z }
8 7 neeq2i 
 |-  ( { y | x R y } =/= { Z } <-> { y | x R y } =/= { y | y = Z } )
9 nabbib 
 |-  ( { y | x R y } =/= { y | y = Z } <-> E. y ( x R y <-> -. y = Z ) )
10 6 8 9 3bitri 
 |-  ( ( R " { x } ) =/= { Z } <-> E. y ( x R y <-> -. y = Z ) )
11 3 10 anbi12i 
 |-  ( ( x e. dom R /\ ( R " { x } ) =/= { Z } ) <-> ( E. y x R y /\ E. y ( x R y <-> -. y = Z ) ) )
12 11 abbii 
 |-  { x | ( x e. dom R /\ ( R " { x } ) =/= { Z } ) } = { x | ( E. y x R y /\ E. y ( x R y <-> -. y = Z ) ) }
13 1 12 eqtr2i 
 |-  { x | ( E. y x R y /\ E. y ( x R y <-> -. y = Z ) ) } = { x e. dom R | ( R " { x } ) =/= { Z } }
14 13 a1i 
 |-  ( ( R e. V /\ Z e. W ) -> { x | ( E. y x R y /\ E. y ( x R y <-> -. y = Z ) ) } = { x e. dom R | ( R " { x } ) =/= { Z } } )
15 df-ne 
 |-  ( y =/= Z <-> -. y = Z )
16 15 bibi2i 
 |-  ( ( x R y <-> y =/= Z ) <-> ( x R y <-> -. y = Z ) )
17 16 exbii 
 |-  ( E. y ( x R y <-> y =/= Z ) <-> E. y ( x R y <-> -. y = Z ) )
18 17 anbi2i 
 |-  ( ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) <-> ( E. y x R y /\ E. y ( x R y <-> -. y = Z ) ) )
19 18 abbii 
 |-  { x | ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) } = { x | ( E. y x R y /\ E. y ( x R y <-> -. y = Z ) ) }
20 19 a1i 
 |-  ( ( R e. V /\ Z e. W ) -> { x | ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) } = { x | ( E. y x R y /\ E. y ( x R y <-> -. y = Z ) ) } )
21 suppval 
 |-  ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = { x e. dom R | ( R " { x } ) =/= { Z } } )
22 14 20 21 3eqtr4rd 
 |-  ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = { x | ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) } )