MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  suppvalbr Structured version   Visualization version   Unicode version

Theorem suppvalbr 6915
Description: The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019.)
Assertion
Ref Expression
suppvalbr  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( R supp  Z )  =  { x  |  ( E. y  x R y  /\  E. y ( x R y  <->  y  =/=  Z
) ) } )
Distinct variable groups:    x, R, y    x, Z, y
Allowed substitution hints:    V( x, y)    W( x, y)

Proof of Theorem suppvalbr
StepHypRef Expression
1 suppval 6913 . 2  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( R supp  Z )  =  { x  e. 
dom  R  |  ( R " { x }
)  =/=  { Z } } )
2 df-rab 2745 . . . 4  |-  { x  e.  dom  R  |  ( R " { x } )  =/=  { Z } }  =  {
x  |  ( x  e.  dom  R  /\  ( R " { x } )  =/=  { Z } ) }
3 vex 3047 . . . . . . 7  |-  x  e. 
_V
43eldm 5031 . . . . . 6  |-  ( x  e.  dom  R  <->  E. y  x R y )
5 df-sn 3968 . . . . . . . 8  |-  { Z }  =  { y  |  y  =  Z }
65neeq2i 2688 . . . . . . 7  |-  ( { y  |  x R y }  =/=  { Z }  <->  { y  |  x R y }  =/=  { y  |  y  =  Z } )
7 imasng 5189 . . . . . . . . 9  |-  ( x  e.  _V  ->  ( R " { x }
)  =  { y  |  x R y } )
83, 7ax-mp 5 . . . . . . . 8  |-  ( R
" { x }
)  =  { y  |  x R y }
98neeq1i 2687 . . . . . . 7  |-  ( ( R " { x } )  =/=  { Z }  <->  { y  |  x R y }  =/=  { Z } )
10 nabbi 2724 . . . . . . 7  |-  ( E. y ( x R y  <->  -.  y  =  Z )  <->  { y  |  x R y }  =/=  { y  |  y  =  Z }
)
116, 9, 103bitr4i 281 . . . . . 6  |-  ( ( R " { x } )  =/=  { Z }  <->  E. y ( x R y  <->  -.  y  =  Z ) )
124, 11anbi12i 702 . . . . 5  |-  ( ( x  e.  dom  R  /\  ( R " {
x } )  =/= 
{ Z } )  <-> 
( E. y  x R y  /\  E. y ( x R y  <->  -.  y  =  Z ) ) )
1312abbii 2566 . . . 4  |-  { x  |  ( x  e. 
dom  R  /\  ( R " { x }
)  =/=  { Z } ) }  =  { x  |  ( E. y  x R
y  /\  E. y
( x R y  <->  -.  y  =  Z
) ) }
142, 13eqtri 2472 . . 3  |-  { x  e.  dom  R  |  ( R " { x } )  =/=  { Z } }  =  {
x  |  ( E. y  x R y  /\  E. y ( x R y  <->  -.  y  =  Z ) ) }
1514a1i 11 . 2  |-  ( ( 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 2623 . . . . . . . 8  |-  ( y  =/=  Z  <->  -.  y  =  Z )
1716bicomi 206 . . . . . . 7  |-  ( -.  y  =  Z  <->  y  =/=  Z )
1817bibi2i 315 . . . . . 6  |-  ( ( x R y  <->  -.  y  =  Z )  <->  ( x R y  <->  y  =/=  Z ) )
1918exbii 1717 . . . . 5  |-  ( E. y ( x R y  <->  -.  y  =  Z )  <->  E. y
( x R y  <-> 
y  =/=  Z ) )
2019anbi2i 699 . . . 4  |-  ( ( E. y  x R y  /\  E. y
( x R y  <->  -.  y  =  Z
) )  <->  ( E. y  x R y  /\  E. y ( x R y  <->  y  =/=  Z
) ) )
2120abbii 2566 . . 3  |-  { 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
) ) }
2221a1i 11 . 2  |-  ( ( 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 ) ) } )
231, 15, 223eqtrd 2488 1  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( R supp  Z )  =  { x  |  ( E. y  x R y  /\  E. y ( x R y  <->  y  =/=  Z
) ) } )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1443   E.wex 1662    e. wcel 1886   {cab 2436    =/= wne 2621   {crab 2740   _Vcvv 3044   {csn 3967   class class class wbr 4401   dom cdm 4833   "cima 4836  (class class class)co 6288   supp csupp 6911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638  ax-un 6580
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fv 5589  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-supp 6912
This theorem is referenced by:  suppimacnvss  6921  suppimacnv  6922
  Copyright terms: Public domain W3C validator