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

Theorem fnsuppres 6919
Description: Two ways to express restriction of a support set. (Contributed by Stefan O'Rear, 5-Feb-2015.) (Revised by AV, 28-May-2019.)
Assertion
Ref Expression
fnsuppres  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( ( F supp 
Z )  C_  A  <->  ( F  |`  B )  =  ( B  X.  { Z } ) ) )

Proof of Theorem fnsuppres
Dummy variable  a is distinct from all other variables.
StepHypRef Expression
1 fndm 5673 . . . . . 6  |-  ( F  Fn  ( A  u.  B )  ->  dom  F  =  ( A  u.  B ) )
2 rabeq 3102 . . . . . 6  |-  ( dom 
F  =  ( A  u.  B )  ->  { a  e.  dom  F  |  ( F `  a )  =/=  Z }  =  { a  e.  ( A  u.  B
)  |  ( F `
 a )  =/= 
Z } )
31, 2syl 16 . . . . 5  |-  ( F  Fn  ( A  u.  B )  ->  { a  e.  dom  F  | 
( F `  a
)  =/=  Z }  =  { a  e.  ( A  u.  B )  |  ( F `  a )  =/=  Z } )
433ad2ant1 1012 . . . 4  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  { a  e. 
dom  F  |  ( F `  a )  =/=  Z }  =  {
a  e.  ( A  u.  B )  |  ( F `  a
)  =/=  Z }
)
54sseq1d 3526 . . 3  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( { a  e.  dom  F  | 
( F `  a
)  =/=  Z }  C_  A  <->  { a  e.  ( A  u.  B )  |  ( F `  a )  =/=  Z }  C_  A ) )
6 unss 3673 . . . . 5  |-  ( ( { a  e.  A  |  ( F `  a )  =/=  Z }  C_  A  /\  {
a  e.  B  | 
( F `  a
)  =/=  Z }  C_  A )  <->  ( {
a  e.  A  | 
( F `  a
)  =/=  Z }  u.  { a  e.  B  |  ( F `  a )  =/=  Z } )  C_  A
)
7 ssrab2 3580 . . . . . 6  |-  { a  e.  A  |  ( F `  a )  =/=  Z }  C_  A
87biantrur 506 . . . . 5  |-  ( { a  e.  B  | 
( F `  a
)  =/=  Z }  C_  A  <->  ( { a  e.  A  |  ( F `  a )  =/=  Z }  C_  A  /\  { a  e.  B  |  ( F `
 a )  =/= 
Z }  C_  A
) )
9 rabun2 3772 . . . . . 6  |-  { a  e.  ( A  u.  B )  |  ( F `  a )  =/=  Z }  =  ( { a  e.  A  |  ( F `  a )  =/=  Z }  u.  { a  e.  B  |  ( F `  a )  =/=  Z } )
109sseq1i 3523 . . . . 5  |-  ( { a  e.  ( A  u.  B )  |  ( F `  a
)  =/=  Z }  C_  A  <->  ( { a  e.  A  |  ( F `  a )  =/=  Z }  u.  { a  e.  B  | 
( F `  a
)  =/=  Z }
)  C_  A )
116, 8, 103bitr4ri 278 . . . 4  |-  ( { a  e.  ( A  u.  B )  |  ( F `  a
)  =/=  Z }  C_  A  <->  { a  e.  B  |  ( F `  a )  =/=  Z }  C_  A )
12 rabss 3572 . . . . 5  |-  ( { a  e.  B  | 
( F `  a
)  =/=  Z }  C_  A  <->  A. a  e.  B  ( ( F `  a )  =/=  Z  ->  a  e.  A ) )
13 fvres 5873 . . . . . . . . 9  |-  ( a  e.  B  ->  (
( F  |`  B ) `
 a )  =  ( F `  a
) )
1413adantl 466 . . . . . . . 8  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  /\  a  e.  B
)  ->  ( ( F  |`  B ) `  a )  =  ( F `  a ) )
15 simp2r 1018 . . . . . . . . 9  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  Z  e.  V
)
16 fvconst2g 6107 . . . . . . . . 9  |-  ( ( Z  e.  V  /\  a  e.  B )  ->  ( ( B  X.  { Z } ) `  a )  =  Z )
1715, 16sylan 471 . . . . . . . 8  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  /\  a  e.  B
)  ->  ( ( B  X.  { Z }
) `  a )  =  Z )
1814, 17eqeq12d 2484 . . . . . . 7  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  /\  a  e.  B
)  ->  ( (
( F  |`  B ) `
 a )  =  ( ( B  X.  { Z } ) `  a )  <->  ( F `  a )  =  Z ) )
19 nne 2663 . . . . . . . 8  |-  ( -.  ( F `  a
)  =/=  Z  <->  ( F `  a )  =  Z )
2019a1i 11 . . . . . . 7  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  /\  a  e.  B
)  ->  ( -.  ( F `  a )  =/=  Z  <->  ( F `  a )  =  Z ) )
21 id 22 . . . . . . . . 9  |-  ( a  e.  B  ->  a  e.  B )
22 simp3 993 . . . . . . . . 9  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( A  i^i  B )  =  (/) )
23 minel 3877 . . . . . . . . 9  |-  ( ( a  e.  B  /\  ( A  i^i  B )  =  (/) )  ->  -.  a  e.  A )
2421, 22, 23syl2anr 478 . . . . . . . 8  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  /\  a  e.  B
)  ->  -.  a  e.  A )
25 mtt 339 . . . . . . . 8  |-  ( -.  a  e.  A  -> 
( -.  ( F `
 a )  =/= 
Z  <->  ( ( F `
 a )  =/= 
Z  ->  a  e.  A ) ) )
2624, 25syl 16 . . . . . . 7  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  /\  a  e.  B
)  ->  ( -.  ( F `  a )  =/=  Z  <->  ( ( F `  a )  =/=  Z  ->  a  e.  A ) ) )
2718, 20, 263bitr2rd 282 . . . . . 6  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  /\  a  e.  B
)  ->  ( (
( F `  a
)  =/=  Z  -> 
a  e.  A )  <-> 
( ( F  |`  B ) `  a
)  =  ( ( B  X.  { Z } ) `  a
) ) )
2827ralbidva 2895 . . . . 5  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( A. a  e.  B  ( ( F `  a )  =/=  Z  ->  a  e.  A )  <->  A. a  e.  B  ( ( F  |`  B ) `  a )  =  ( ( B  X.  { Z } ) `  a
) ) )
2912, 28syl5bb 257 . . . 4  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( { a  e.  B  |  ( F `  a )  =/=  Z }  C_  A 
<-> 
A. a  e.  B  ( ( F  |`  B ) `  a
)  =  ( ( B  X.  { Z } ) `  a
) ) )
3011, 29syl5bb 257 . . 3  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( { a  e.  ( A  u.  B )  |  ( F `  a )  =/=  Z }  C_  A 
<-> 
A. a  e.  B  ( ( F  |`  B ) `  a
)  =  ( ( B  X.  { Z } ) `  a
) ) )
315, 30bitrd 253 . 2  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( { a  e.  dom  F  | 
( F `  a
)  =/=  Z }  C_  A  <->  A. a  e.  B  ( ( F  |`  B ) `  a
)  =  ( ( B  X.  { Z } ) `  a
) ) )
32 fnfun 5671 . . . . . . 7  |-  ( F  Fn  ( A  u.  B )  ->  Fun  F )
33323anim1i 1177 . . . . . 6  |-  ( ( F  Fn  ( A  u.  B )  /\  F  e.  W  /\  Z  e.  V )  ->  ( Fun  F  /\  F  e.  W  /\  Z  e.  V )
)
34333expb 1192 . . . . 5  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
) )  ->  ( Fun  F  /\  F  e.  W  /\  Z  e.  V ) )
35 suppval1 6899 . . . . 5  |-  ( ( Fun  F  /\  F  e.  W  /\  Z  e.  V )  ->  ( F supp  Z )  =  {
a  e.  dom  F  |  ( F `  a )  =/=  Z } )
3634, 35syl 16 . . . 4  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
) )  ->  ( F supp  Z )  =  {
a  e.  dom  F  |  ( F `  a )  =/=  Z } )
37363adant3 1011 . . 3  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( F supp  Z
)  =  { a  e.  dom  F  | 
( F `  a
)  =/=  Z }
)
3837sseq1d 3526 . 2  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( ( F supp 
Z )  C_  A  <->  { a  e.  dom  F  |  ( F `  a )  =/=  Z }  C_  A ) )
39 simp1 991 . . . 4  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  F  Fn  ( A  u.  B )
)
40 ssun2 3663 . . . . 5  |-  B  C_  ( A  u.  B
)
4140a1i 11 . . . 4  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  B  C_  ( A  u.  B )
)
42 fnssres 5687 . . . 4  |-  ( ( F  Fn  ( A  u.  B )  /\  B  C_  ( A  u.  B ) )  -> 
( F  |`  B )  Fn  B )
4339, 41, 42syl2anc 661 . . 3  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( F  |`  B )  Fn  B
)
44 fnconstg 5766 . . . . 5  |-  ( Z  e.  V  ->  ( B  X.  { Z }
)  Fn  B )
4544adantl 466 . . . 4  |-  ( ( F  e.  W  /\  Z  e.  V )  ->  ( B  X.  { Z } )  Fn  B
)
46453ad2ant2 1013 . . 3  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( B  X.  { Z } )  Fn  B )
47 eqfnfv 5968 . . 3  |-  ( ( ( F  |`  B )  Fn  B  /\  ( B  X.  { Z }
)  Fn  B )  ->  ( ( F  |`  B )  =  ( B  X.  { Z } )  <->  A. a  e.  B  ( ( F  |`  B ) `  a )  =  ( ( B  X.  { Z } ) `  a
) ) )
4843, 46, 47syl2anc 661 . 2  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( ( F  |`  B )  =  ( B  X.  { Z } )  <->  A. a  e.  B  ( ( F  |`  B ) `  a )  =  ( ( B  X.  { Z } ) `  a
) ) )
4931, 38, 483bitr4d 285 1  |-  ( ( F  Fn  ( A  u.  B )  /\  ( F  e.  W  /\  Z  e.  V
)  /\  ( A  i^i  B )  =  (/) )  ->  ( ( F supp 
Z )  C_  A  <->  ( F  |`  B )  =  ( B  X.  { Z } ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 968    = wceq 1374    e. wcel 1762    =/= wne 2657   A.wral 2809   {crab 2813    u. cun 3469    i^i cin 3470    C_ wss 3471   (/)c0 3780   {csn 4022    X. cxp 4992   dom cdm 4994    |` cres 4996   Fun wfun 5575    Fn wfn 5576   ` cfv 5581  (class class class)co 6277   supp csupp 6893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pow 4620  ax-pr 4681  ax-un 6569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-opab 4501  df-mpt 4502  df-id 4790  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-rn 5005  df-res 5006  df-ima 5007  df-iota 5544  df-fun 5583  df-fn 5584  df-f 5585  df-fv 5589  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-supp 6894
This theorem is referenced by:  fnsuppeq0  6920  frlmsslss2  18567  resf1o  27213
  Copyright terms: Public domain W3C validator