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

Theorem suppimacnv 6902
Description: Support sets of functions expressed by inverse images. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 7-Apr-2019.)
Assertion
Ref Expression
suppimacnv  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( R supp  Z )  =  ( `' R " ( _V  \  { Z } ) ) )

Proof of Theorem suppimacnv
Dummy variables  x  y  s  t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 4443 . . . . . . . 8  |-  ( t  =  s  ->  (
x R t  <->  x R
s ) )
21cbvexvw 1815 . . . . . . 7  |-  ( E. t  x R t  <->  E. s  x R
s )
3 breq2 4443 . . . . . . . . . . . . . 14  |-  ( s  =  Z  ->  (
x R s  <->  x R Z ) )
43anbi1d 702 . . . . . . . . . . . . 13  |-  ( s  =  Z  ->  (
( x R s  /\  ( x R t  <->  t  =/=  Z
) )  <->  ( x R Z  /\  (
x R t  <->  t  =/=  Z ) ) ) )
5 bianir 965 . . . . . . . . . . . . . . . . . 18  |-  ( ( t  =/=  Z  /\  ( x R t  <-> 
t  =/=  Z ) )  ->  x R
t )
6 vex 3109 . . . . . . . . . . . . . . . . . . . 20  |-  t  e. 
_V
7 breq2 4443 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  t  ->  (
x R y  <->  x R
t ) )
8 neeq1 2735 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  t  ->  (
y  =/=  Z  <->  t  =/=  Z ) )
97, 8anbi12d 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  t  ->  (
( x R y  /\  y  =/=  Z
)  <->  ( x R t  /\  t  =/= 
Z ) ) )
106, 9spcev 3198 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x R t  /\  t  =/=  Z )  ->  E. y ( x R y  /\  y  =/= 
Z ) )
1110ex 432 . . . . . . . . . . . . . . . . . 18  |-  ( x R t  ->  (
t  =/=  Z  ->  E. y ( x R y  /\  y  =/= 
Z ) ) )
125, 11syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( t  =/=  Z  /\  ( x R t  <-> 
t  =/=  Z ) )  ->  ( t  =/=  Z  ->  E. y
( x R y  /\  y  =/=  Z
) ) )
1312ex 432 . . . . . . . . . . . . . . . 16  |-  ( t  =/=  Z  ->  (
( x R t  <-> 
t  =/=  Z )  ->  ( t  =/= 
Z  ->  E. y
( x R y  /\  y  =/=  Z
) ) ) )
1413pm2.43a 49 . . . . . . . . . . . . . . 15  |-  ( t  =/=  Z  ->  (
( x R t  <-> 
t  =/=  Z )  ->  E. y ( x R y  /\  y  =/=  Z ) ) )
1514adantld 465 . . . . . . . . . . . . . 14  |-  ( t  =/=  Z  ->  (
( x R Z  /\  ( x R t  <->  t  =/=  Z
) )  ->  E. y
( x R y  /\  y  =/=  Z
) ) )
16 nne 2655 . . . . . . . . . . . . . . . 16  |-  ( -.  t  =/=  Z  <->  t  =  Z )
17 notbi 293 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x R t  <->  t  =/=  Z )  <->  ( -.  x R t  <->  -.  t  =/=  Z ) )
18 bianir 965 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( -.  t  =/=  Z  /\  ( -.  x R t  <->  -.  t  =/=  Z ) )  ->  -.  x R t )
19 breq2 4443 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( Z  =  t  ->  (
x R Z  <->  x R
t ) )
2019eqcoms 2466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  Z  ->  (
x R Z  <->  x R
t ) )
21 pm2.24 109 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x R t  ->  ( -.  x R t  ->  E. y ( x R y  /\  y  =/= 
Z ) ) )
2220, 21syl6bi 228 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  =  Z  ->  (
x R Z  -> 
( -.  x R t  ->  E. y
( x R y  /\  y  =/=  Z
) ) ) )
2322com13 80 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  x R t  -> 
( x R Z  ->  ( t  =  Z  ->  E. y
( x R y  /\  y  =/=  Z
) ) ) )
2418, 23syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( -.  t  =/=  Z  /\  ( -.  x R t  <->  -.  t  =/=  Z ) )  ->  (
x R Z  -> 
( t  =  Z  ->  E. y ( x R y  /\  y  =/=  Z ) ) ) )
2524ex 432 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  t  =/=  Z  -> 
( ( -.  x R t  <->  -.  t  =/=  Z )  ->  (
x R Z  -> 
( t  =  Z  ->  E. y ( x R y  /\  y  =/=  Z ) ) ) ) )
2617, 25syl5bi 217 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  t  =/=  Z  -> 
( ( x R t  <->  t  =/=  Z
)  ->  ( x R Z  ->  ( t  =  Z  ->  E. y
( x R y  /\  y  =/=  Z
) ) ) ) )
2726com13 80 . . . . . . . . . . . . . . . . . 18  |-  ( x R Z  ->  (
( x R t  <-> 
t  =/=  Z )  ->  ( -.  t  =/=  Z  ->  ( t  =  Z  ->  E. y
( x R y  /\  y  =/=  Z
) ) ) ) )
2827imp 427 . . . . . . . . . . . . . . . . 17  |-  ( ( x R Z  /\  ( x R t  <-> 
t  =/=  Z ) )  ->  ( -.  t  =/=  Z  ->  (
t  =  Z  ->  E. y ( x R y  /\  y  =/= 
Z ) ) ) )
2928com13 80 . . . . . . . . . . . . . . . 16  |-  ( t  =  Z  ->  ( -.  t  =/=  Z  ->  ( ( x R Z  /\  ( x R t  <->  t  =/=  Z ) )  ->  E. y
( x R y  /\  y  =/=  Z
) ) ) )
3016, 29sylbi 195 . . . . . . . . . . . . . . 15  |-  ( -.  t  =/=  Z  -> 
( -.  t  =/= 
Z  ->  ( (
x R Z  /\  ( x R t  <-> 
t  =/=  Z ) )  ->  E. y
( x R y  /\  y  =/=  Z
) ) ) )
3130pm2.43i 47 . . . . . . . . . . . . . 14  |-  ( -.  t  =/=  Z  -> 
( ( x R Z  /\  ( x R t  <->  t  =/=  Z ) )  ->  E. y
( x R y  /\  y  =/=  Z
) ) )
3215, 31pm2.61i 164 . . . . . . . . . . . . 13  |-  ( ( x R Z  /\  ( x R t  <-> 
t  =/=  Z ) )  ->  E. y
( x R y  /\  y  =/=  Z
) )
334, 32syl6bi 228 . . . . . . . . . . . 12  |-  ( s  =  Z  ->  (
( x R s  /\  ( x R t  <->  t  =/=  Z
) )  ->  E. y
( x R y  /\  y  =/=  Z
) ) )
34 vex 3109 . . . . . . . . . . . . . . . 16  |-  s  e. 
_V
35 breq2 4443 . . . . . . . . . . . . . . . . 17  |-  ( y  =  s  ->  (
x R y  <->  x R
s ) )
36 neeq1 2735 . . . . . . . . . . . . . . . . 17  |-  ( y  =  s  ->  (
y  =/=  Z  <->  s  =/=  Z ) )
3735, 36anbi12d 708 . . . . . . . . . . . . . . . 16  |-  ( y  =  s  ->  (
( x R y  /\  y  =/=  Z
)  <->  ( x R s  /\  s  =/= 
Z ) ) )
3834, 37spcev 3198 . . . . . . . . . . . . . . 15  |-  ( ( x R s  /\  s  =/=  Z )  ->  E. y ( x R y  /\  y  =/= 
Z ) )
3938ex 432 . . . . . . . . . . . . . 14  |-  ( x R s  ->  (
s  =/=  Z  ->  E. y ( x R y  /\  y  =/= 
Z ) ) )
4039adantr 463 . . . . . . . . . . . . 13  |-  ( ( x R s  /\  ( x R t  <-> 
t  =/=  Z ) )  ->  ( s  =/=  Z  ->  E. y
( x R y  /\  y  =/=  Z
) ) )
4140com12 31 . . . . . . . . . . . 12  |-  ( s  =/=  Z  ->  (
( x R s  /\  ( x R t  <->  t  =/=  Z
) )  ->  E. y
( x R y  /\  y  =/=  Z
) ) )
4233, 41pm2.61ine 2767 . . . . . . . . . . 11  |-  ( ( x R s  /\  ( x R t  <-> 
t  =/=  Z ) )  ->  E. y
( x R y  /\  y  =/=  Z
) )
4342expcom 433 . . . . . . . . . 10  |-  ( ( x R t  <->  t  =/=  Z )  ->  ( x R s  ->  E. y
( x R y  /\  y  =/=  Z
) ) )
4443exlimiv 1727 . . . . . . . . 9  |-  ( E. t ( x R t  <->  t  =/=  Z
)  ->  ( x R s  ->  E. y
( x R y  /\  y  =/=  Z
) ) )
4544com12 31 . . . . . . . 8  |-  ( x R s  ->  ( E. t ( x R t  <->  t  =/=  Z
)  ->  E. y
( x R y  /\  y  =/=  Z
) ) )
4645exlimiv 1727 . . . . . . 7  |-  ( E. s  x R s  ->  ( E. t
( x R t  <-> 
t  =/=  Z )  ->  E. y ( x R y  /\  y  =/=  Z ) ) )
472, 46sylbi 195 . . . . . 6  |-  ( E. t  x R t  ->  ( E. t
( x R t  <-> 
t  =/=  Z )  ->  E. y ( x R y  /\  y  =/=  Z ) ) )
4847imp 427 . . . . 5  |-  ( ( E. t  x R t  /\  E. t
( x R t  <-> 
t  =/=  Z ) )  ->  E. y
( x R y  /\  y  =/=  Z
) )
4948a1i 11 . . . 4  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( ( E. t  x R t  /\  E. t ( x R t  <->  t  =/=  Z
) )  ->  E. y
( x R y  /\  y  =/=  Z
) ) )
5049ss2abdv 3559 . . 3  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  { x  |  ( E. t  x R t  /\  E. t
( x R t  <-> 
t  =/=  Z ) ) }  C_  { x  |  E. y ( x R y  /\  y  =/=  Z ) } )
51 suppvalbr 6895 . . 3  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( R supp  Z )  =  { x  |  ( E. t  x R t  /\  E. t ( x R t  <->  t  =/=  Z
) ) } )
52 cnvimadfsn 6900 . . . 4  |-  ( `' R " ( _V 
\  { Z }
) )  =  {
x  |  E. y
( x R y  /\  y  =/=  Z
) }
5352a1i 11 . . 3  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( `' R "
( _V  \  { Z } ) )  =  { x  |  E. y ( x R y  /\  y  =/= 
Z ) } )
5450, 51, 533sstr4d 3532 . 2  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( R supp  Z ) 
C_  ( `' R " ( _V  \  { Z } ) ) )
55 suppimacnvss 6901 . 2  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( `' R "
( _V  \  { Z } ) )  C_  ( R supp  Z )
)
5654, 55eqssd 3506 1  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( R supp  Z )  =  ( `' R " ( _V  \  { Z } ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1398   E.wex 1617    e. wcel 1823   {cab 2439    =/= wne 2649   _Vcvv 3106    \ cdif 3458   {csn 4016   class class class wbr 4439   `'ccnv 4987   "cima 4991  (class class class)co 6270   supp csupp 6891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-supp 6892
This theorem is referenced by:  frnsuppeq  6903  suppun  6912  mptsuppdifd  6914  supp0cosupp0  6931  imacosupp  6932  fdmfisuppfi  7830  fsuppun  7840  fsuppco  7853  cantnffvalOLD  8073  gsumval3a  17107  gsumzf1o  17119  gsumzaddlem  17136  gsummptfsaddOLD  17143  gsumzmhm  17158  gsumzoppg  17168  dprdvalOLD  17234  mplvalOLD  18283  mdegfvalOLD  22630  deg1val  22665  suppss3  27784  ffsrn  27786  fpwrelmapffslem  27789  sitgclg  28551  eulerpartlemmf  28581  eulerpartlemgf  28585
  Copyright terms: Public domain W3C validator