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

Theorem suppimacnv 6814
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 4407 . . . . . . . 8  |-  ( t  =  s  ->  (
x R t  <->  x R
s ) )
21cbvexvw 1750 . . . . . . 7  |-  ( E. t  x R t  <->  E. s  x R
s )
3 breq2 4407 . . . . . . . . . . . . . 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 958 . . . . . . . . . . . . . . . . . 18  |-  ( ( t  =/=  Z  /\  ( x R t  <-> 
t  =/=  Z ) )  ->  x R
t )
6 vex 3081 . . . . . . . . . . . . . . . . . . . 20  |-  t  e. 
_V
7 breq2 4407 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  t  ->  (
x R y  <->  x R
t ) )
8 neeq1 2733 . . . . . . . . . . . . . . . . . . . . 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 3170 . . . . . . . . . . . . . . . . . . 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 2654 . . . . . . . . . . . . . . . 16  |-  ( -.  t  =/=  Z  <->  t  =  Z )
17 notbi 295 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x R t  <->  t  =/=  Z )  <->  ( -.  x R t  <->  -.  t  =/=  Z ) )
18 bianir 958 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( -.  t  =/=  Z  /\  ( -.  x R t  <->  -.  t  =/=  Z ) )  ->  -.  x R t )
19 breq2 4407 . . . . . . . . . . . . . . . . . . . . . . . . 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 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 3081 . . . . . . . . . . . . . . . 16  |-  s  e. 
_V
35 breq2 4407 . . . . . . . . . . . . . . . . 17  |-  ( y  =  s  ->  (
x R y  <->  x R
s ) )
36 neeq1 2733 . . . . . . . . . . . . . . . . 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 3170 . . . . . . . . . . . . . . 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 2765 . . . . . . . . . . 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 1689 . . . . . . . . 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 1689 . . . . . . 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 3536 . . 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 6807 . . 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 6812 . . . 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 3510 . 2  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( R supp  Z ) 
C_  ( `' R " ( _V  \  { Z } ) ) )
55 suppimacnvss 6813 . 2  |-  ( ( R  e.  V  /\  Z  e.  W )  ->  ( `' R "
( _V  \  { Z } ) )  C_  ( R supp  Z )
)
5654, 55eqssd 3484 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 1370   E.wex 1587    e. wcel 1758   {cab 2439    =/= wne 2648   _Vcvv 3078    \ cdif 3436   {csn 3988   class class class wbr 4403   `'ccnv 4950   "cima 4954  (class class class)co 6203   supp csupp 6803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642  ax-un 6485
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-opab 4462  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fv 5537  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-supp 6804
This theorem is referenced by:  frnsuppeq  6815  suppun  6822  mptsuppdifd  6824  supp0cosupp0  6841  imacosupp  6842  fdmfisuppfi  7743  fsuppun  7753  fsuppco  7765  cantnffvalOLD  7985  gsumval3a  16503  gsumzf1o  16515  gsumzaddlem  16532  gsummptfsaddOLD  16539  gsumzmhm  16555  gsumzoppg  16565  dprdvalOLD  16612  mplvalOLD  17629  mdegfvalOLD  21668  deg1val  21703  suppss3  26198  ffsrn  26200  fpwrelmapffslem  26203  eulerpartlemmf  26922  eulerpartlemgf  26926
  Copyright terms: Public domain W3C validator