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

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

Proof of Theorem fnsuppres
Dummy variable  a is distinct from all other variables.
StepHypRef Expression
1 unss 3485 . . . 4  |-  ( ( { 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
)
2 ssrab2 3392 . . . . 5  |-  { a  e.  A  |  ( F `  a )  =/=  Z }  C_  A
32biantrur 493 . . . 4  |-  ( { a  e.  B  | 
( F `  a
)  =/=  Z }  C_  A  <->  ( { a  e.  A  |  ( F `  a )  =/=  Z }  C_  A  /\  { a  e.  B  |  ( F `
 a )  =/= 
Z }  C_  A
) )
4 rabun2 3584 . . . . 5  |-  { a  e.  ( A  u.  B )  |  ( F `  a )  =/=  Z }  =  ( { a  e.  A  |  ( F `  a )  =/=  Z }  u.  { a  e.  B  |  ( F `  a )  =/=  Z } )
54sseq1i 3336 . . . 4  |-  ( { 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 )
61, 3, 53bitr4ri 270 . . 3  |-  ( { a  e.  ( A  u.  B )  |  ( F `  a
)  =/=  Z }  C_  A  <->  { a  e.  B  |  ( F `  a )  =/=  Z }  C_  A )
7 rabss 3384 . . . 4  |-  ( { a  e.  B  | 
( F `  a
)  =/=  Z }  C_  A  <->  A. a  e.  B  ( ( F `  a )  =/=  Z  ->  a  e.  A ) )
8 fvres 5708 . . . . . . . 8  |-  ( a  e.  B  ->  (
( F  |`  B ) `
 a )  =  ( F `  a
) )
98adantl 453 . . . . . . 7  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B
)  =  (/)  /\  Z  e.  V )  /\  a  e.  B )  ->  (
( F  |`  B ) `
 a )  =  ( F `  a
) )
10 fvconst2g 5908 . . . . . . . 8  |-  ( ( Z  e.  V  /\  a  e.  B )  ->  ( ( B  X.  { Z } ) `  a )  =  Z )
11103ad2antl3 1121 . . . . . . 7  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B
)  =  (/)  /\  Z  e.  V )  /\  a  e.  B )  ->  (
( B  X.  { Z } ) `  a
)  =  Z )
129, 11eqeq12d 2422 . . . . . 6  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B
)  =  (/)  /\  Z  e.  V )  /\  a  e.  B )  ->  (
( ( F  |`  B ) `  a
)  =  ( ( B  X.  { Z } ) `  a
)  <->  ( F `  a )  =  Z ) )
13 nne 2575 . . . . . . 7  |-  ( -.  ( F `  a
)  =/=  Z  <->  ( F `  a )  =  Z )
1413a1i 11 . . . . . 6  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B
)  =  (/)  /\  Z  e.  V )  /\  a  e.  B )  ->  ( -.  ( F `  a
)  =/=  Z  <->  ( F `  a )  =  Z ) )
15 id 20 . . . . . . . 8  |-  ( a  e.  B  ->  a  e.  B )
16 simp2 958 . . . . . . . 8  |-  ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B )  =  (/)  /\  Z  e.  V )  ->  ( A  i^i  B )  =  (/) )
17 minel 3647 . . . . . . . 8  |-  ( ( a  e.  B  /\  ( A  i^i  B )  =  (/) )  ->  -.  a  e.  A )
1815, 16, 17syl2anr 465 . . . . . . 7  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B
)  =  (/)  /\  Z  e.  V )  /\  a  e.  B )  ->  -.  a  e.  A )
19 mtt 330 . . . . . . 7  |-  ( -.  a  e.  A  -> 
( -.  ( F `
 a )  =/= 
Z  <->  ( ( F `
 a )  =/= 
Z  ->  a  e.  A ) ) )
2018, 19syl 16 . . . . . 6  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B
)  =  (/)  /\  Z  e.  V )  /\  a  e.  B )  ->  ( -.  ( F `  a
)  =/=  Z  <->  ( ( F `  a )  =/=  Z  ->  a  e.  A ) ) )
2112, 14, 203bitr2rd 274 . . . . 5  |-  ( ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B
)  =  (/)  /\  Z  e.  V )  /\  a  e.  B )  ->  (
( ( F `  a )  =/=  Z  ->  a  e.  A )  <-> 
( ( F  |`  B ) `  a
)  =  ( ( B  X.  { Z } ) `  a
) ) )
2221ralbidva 2686 . . . 4  |-  ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B )  =  (/)  /\  Z  e.  V )  ->  ( A. a  e.  B  ( ( F `  a )  =/=  Z  ->  a  e.  A )  <->  A. a  e.  B  ( ( F  |`  B ) `  a
)  =  ( ( B  X.  { Z } ) `  a
) ) )
237, 22syl5bb 249 . . 3  |-  ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B )  =  (/)  /\  Z  e.  V )  ->  ( { a  e.  B  |  ( F `  a )  =/=  Z }  C_  A  <->  A. a  e.  B  ( ( F  |`  B ) `  a )  =  ( ( B  X.  { Z } ) `  a
) ) )
246, 23syl5bb 249 . 2  |-  ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B )  =  (/)  /\  Z  e.  V )  ->  ( { a  e.  ( A  u.  B )  |  ( F `  a )  =/=  Z }  C_  A  <->  A. a  e.  B  ( ( F  |`  B ) `  a )  =  ( ( B  X.  { Z } ) `  a
) ) )
25 fnniniseg2 5817 . . . 4  |-  ( F  Fn  ( A  u.  B )  ->  ( `' F " ( _V 
\  { Z }
) )  =  {
a  e.  ( A  u.  B )  |  ( F `  a
)  =/=  Z }
)
26253ad2ant1 978 . . 3  |-  ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B )  =  (/)  /\  Z  e.  V )  ->  ( `' F " ( _V 
\  { Z }
) )  =  {
a  e.  ( A  u.  B )  |  ( F `  a
)  =/=  Z }
)
2726sseq1d 3339 . 2  |-  ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B )  =  (/)  /\  Z  e.  V )  ->  (
( `' F "
( _V  \  { Z } ) )  C_  A 
<->  { a  e.  ( A  u.  B )  |  ( F `  a )  =/=  Z }  C_  A ) )
28 simp1 957 . . . 4  |-  ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B )  =  (/)  /\  Z  e.  V )  ->  F  Fn  ( A  u.  B
) )
29 ssun2 3475 . . . . 5  |-  B  C_  ( A  u.  B
)
3029a1i 11 . . . 4  |-  ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B )  =  (/)  /\  Z  e.  V )  ->  B  C_  ( A  u.  B
) )
31 fnssres 5521 . . . 4  |-  ( ( F  Fn  ( A  u.  B )  /\  B  C_  ( A  u.  B ) )  -> 
( F  |`  B )  Fn  B )
3228, 30, 31syl2anc 643 . . 3  |-  ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B )  =  (/)  /\  Z  e.  V )  ->  ( F  |`  B )  Fn  B )
33 fnconstg 5594 . . . 4  |-  ( Z  e.  V  ->  ( B  X.  { Z }
)  Fn  B )
34333ad2ant3 980 . . 3  |-  ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B )  =  (/)  /\  Z  e.  V )  ->  ( B  X.  { Z }
)  Fn  B )
35 eqfnfv 5790 . . 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
) ) )
3632, 34, 35syl2anc 643 . 2  |-  ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B )  =  (/)  /\  Z  e.  V )  ->  (
( F  |`  B )  =  ( B  X.  { Z } )  <->  A. a  e.  B  ( ( F  |`  B ) `  a )  =  ( ( B  X.  { Z } ) `  a
) ) )
3724, 27, 363bitr4d 277 1  |-  ( ( F  Fn  ( A  u.  B )  /\  ( A  i^i  B )  =  (/)  /\  Z  e.  V )  ->  (
( `' F "
( _V  \  { Z } ) )  C_  A 
<->  ( F  |`  B )  =  ( B  X.  { Z } ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721    =/= wne 2571   A.wral 2670   {crab 2674   _Vcvv 2920    \ cdif 3281    u. cun 3282    i^i cin 3283    C_ wss 3284   (/)c0 3592   {csn 3778    X. cxp 4839   `'ccnv 4840    |` cres 4843   "cima 4844    Fn wfn 5412   ` cfv 5417
This theorem is referenced by:  fnsuppeq0  5916  frlmsslss2  27117
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-fv 5425
  Copyright terms: Public domain W3C validator