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

Theorem suppimacnv 6924
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 4457 . . . . . . . 8  |-  ( t  =  s  ->  (
x R t  <->  x R
s ) )
21cbvexvw 1759 . . . . . . 7  |-  ( E. t  x R t  <->  E. s  x R
s )
3 breq2 4457 . . . . . . . . . . . . . 14  |-  ( s  =  Z  ->  (
x R s  <->  x R Z ) )
43anbi1d 704 . . . . . . . . . . . . 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 3121 . . . . . . . . . . . . . . . . . . . 20  |-  t  e. 
_V
7 breq2 4457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  t  ->  (
x R y  <->  x R
t ) )
8 neeq1 2748 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  t  ->  (
y  =/=  Z  <->  t  =/=  Z ) )
97, 8anbi12d 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  t  ->  (
( x R y  /\  y  =/=  Z
)  <->  ( x R t  /\  t  =/= 
Z ) ) )
106, 9spcev 3210 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x R t  /\  t  =/=  Z )  ->  E. y ( x R y  /\  y  =/= 
Z ) )
1110ex 434 . . . . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . 14  |-  ( t  =/=  Z  ->  (
( x R Z  /\  ( x R t  <->  t  =/=  Z
) )  ->  E. y
( x R y  /\  y  =/=  Z
) ) )
16 nne 2668 . . . . . . . . . . . . . . . 16  |-  ( -.  t  =/=  Z  <->  t  =  Z )
17 notbi 295 . . . . . . . . . . . . . . . . . . . 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 4457 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( Z  =  t  ->  (
x R Z  <->  x R
t ) )
2019eqcoms 2479 . . . . . . . . . . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . . . . 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 3121 . . . . . . . . . . . . . . . 16  |-  s  e. 
_V
35 breq2 4457 . . . . . . . . . . . . . . . . 17  |-  ( y  =  s  ->  (
x R y  <->  x R
s ) )
36 neeq1 2748 . . . . . . . . . . . . . . . . 17  |-  ( y  =  s  ->  (
y  =/=  Z  <->  s  =/=  Z ) )
3735, 36anbi12d 710 . . . . . . . . . . . . . . . 16  |-  ( y  =  s  ->  (
( x R y  /\  y  =/=  Z
)  <->  ( x R s  /\  s  =/= 
Z ) ) )
3834, 37spcev 3210 . . . . . . . . . . . . . . 15  |-  ( ( x R s  /\  s  =/=  Z )  ->  E. y ( x R y  /\  y  =/= 
Z ) )
3938ex 434 . . . . . . . . . . . . . 14  |-  ( x R s  ->  (
s  =/=  Z  ->  E. y ( x R y  /\  y  =/= 
Z ) ) )
4039adantr 465 . . . . . . . . . . . . 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 2780 . . . . . . . . . . 11  |-  ( ( x R s  /\  ( x R t  <-> 
t  =/=  Z ) )  ->  E. y
( x R y  /\  y  =/=  Z
) )
4342expcom 435 . . . . . . . . . 10  |-  ( ( x R t  <->  t  =/=  Z )  ->  ( x R s  ->  E. y
( x R y  /\  y  =/=  Z
) ) )
4443exlimiv 1698 . . . . . . . . 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 1698 . . . . . . 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 429 . . . . 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 3578 . . 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 6917 . . 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 6922 . . . 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 3552 . 2  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( R supp  Z ) 
C_  ( `' R " ( _V  \  { Z } ) ) )
55 suppimacnvss 6923 . 2  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( `' R "
( _V  \  { Z } ) )  C_  ( R supp  Z )
)
5654, 55eqssd 3526 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 369    = wceq 1379   E.wex 1596    e. wcel 1767   {cab 2452    =/= wne 2662   _Vcvv 3118    \ cdif 3478   {csn 4033   class class class wbr 4453   `'ccnv 5004   "cima 5008  (class class class)co 6295   supp csupp 6913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pr 4692  ax-un 6587
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fv 5602  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-supp 6914
This theorem is referenced by:  frnsuppeq  6925  suppun  6932  mptsuppdifd  6934  supp0cosupp0  6951  imacosupp  6952  fdmfisuppfi  7850  fsuppun  7860  fsuppco  7873  cantnffvalOLD  8094  gsumval3a  16778  gsumzf1o  16790  gsumzaddlem  16807  gsummptfsaddOLD  16814  gsumzmhm  16830  gsumzoppg  16840  dprdvalOLD  16909  mplvalOLD  17955  mdegfvalOLD  22329  deg1val  22364  suppss3  27373  ffsrn  27375  fpwrelmapffslem  27378  sitgclg  28109  eulerpartlemmf  28139  eulerpartlemgf  28143
  Copyright terms: Public domain W3C validator