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 suppval 
 |-  ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = { x e. dom R | ( R " { x } ) =/= { Z } } )
2 df-rab 
 |-  { x e. dom R | ( R " { x } ) =/= { Z } } = { x | ( x e. dom R /\ ( R " { x } ) =/= { Z } ) }
3 vex 
 |-  x e. _V
4 3 eldm 
 |-  ( x e. dom R <-> E. y x R y )
5 df-sn 
 |-  { Z } = { y | y = Z }
6 5 neeq2i 
 |-  ( { y | x R y } =/= { Z } <-> { y | x R y } =/= { y | y = Z } )
7 imasng 
 |-  ( x e. _V -> ( R " { x } ) = { y | x R y } )
8 7 elv 
 |-  ( R " { x } ) = { y | x R y }
9 8 neeq1i 
 |-  ( ( R " { x } ) =/= { Z } <-> { y | x R y } =/= { Z } )
10 nabbi 
 |-  ( E. y ( x R y <-> -. y = Z ) <-> { y | x R y } =/= { y | y = Z } )
11 6 9 10 3bitr4i 
 |-  ( ( R " { x } ) =/= { Z } <-> E. y ( x R y <-> -. y = Z ) )
12 4 11 anbi12i 
 |-  ( ( x e. dom R /\ ( R " { x } ) =/= { Z } ) <-> ( E. y x R y /\ E. y ( x R y <-> -. y = Z ) ) )
13 12 abbii 
 |-  { x | ( x e. dom R /\ ( R " { x } ) =/= { Z } ) } = { x | ( E. y x R y /\ E. y ( x R y <-> -. y = Z ) ) }
14 2 13 eqtri 
 |-  { x e. dom R | ( R " { x } ) =/= { Z } } = { x | ( E. y x R y /\ E. y ( x R y <-> -. y = Z ) ) }
15 14 a1i 
 |-  ( ( R e. V /\ Z e. W ) -> { x e. dom R | ( R " { x } ) =/= { Z } } = { x | ( E. y x R y /\ E. y ( x R y <-> -. y = Z ) ) } )
16 df-ne 
 |-  ( y =/= Z <-> -. y = Z )
17 16 bicomi 
 |-  ( -. y = Z <-> y =/= Z )
18 17 bibi2i 
 |-  ( ( x R y <-> -. y = Z ) <-> ( x R y <-> y =/= Z ) )
19 18 exbii 
 |-  ( E. y ( x R y <-> -. y = Z ) <-> E. y ( x R y <-> y =/= Z ) )
20 19 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 ) ) )
21 20 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 ) ) }
22 21 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 ) ) } )
23 1 15 22 3eqtrd 
 |-  ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = { x | ( E. y x R y /\ E. y ( x R y <-> y =/= Z ) ) } )