Metamath Proof Explorer

Theorem ressuppss

Description: The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019)

Ref Expression
Assertion ressuppss 
|- ( ( F e. V /\ Z e. W ) -> ( ( F |` B ) supp Z ) C_ ( F supp Z ) )

Proof

Step Hyp Ref Expression
1 elinel2 
 |-  ( b e. ( B i^i dom F ) -> b e. dom F )
2 dmres 
 |-  dom ( F |` B ) = ( B i^i dom F )
3 1 2 eleq2s 
 |-  ( b e. dom ( F |` B ) -> b e. dom F )
4 3 ad2antrl 
 |-  ( ( ( F e. V /\ Z e. W ) /\ ( b e. dom ( F |` B ) /\ ( ( F |` B ) " { b } ) =/= { Z } ) ) -> b e. dom F )
5 snssi 
 |-  ( b e. B -> { b } C_ B )
6 resima2 
 |-  ( { b } C_ B -> ( ( F |` B ) " { b } ) = ( F " { b } ) )
7 5 6 syl 
 |-  ( b e. B -> ( ( F |` B ) " { b } ) = ( F " { b } ) )
8 7 neeq1d 
 |-  ( b e. B -> ( ( ( F |` B ) " { b } ) =/= { Z } <-> ( F " { b } ) =/= { Z } ) )
9 8 biimpd 
 |-  ( b e. B -> ( ( ( F |` B ) " { b } ) =/= { Z } -> ( F " { b } ) =/= { Z } ) )
10 9 adantld 
 |-  ( b e. B -> ( ( b e. dom ( F |` B ) /\ ( ( F |` B ) " { b } ) =/= { Z } ) -> ( F " { b } ) =/= { Z } ) )
11 10 adantld 
 |-  ( b e. B -> ( ( ( F e. V /\ Z e. W ) /\ ( b e. dom ( F |` B ) /\ ( ( F |` B ) " { b } ) =/= { Z } ) ) -> ( F " { b } ) =/= { Z } ) )
12 elin 
 |-  ( b e. ( B i^i dom F ) <-> ( b e. B /\ b e. dom F ) )
13 pm2.24 
 |-  ( b e. B -> ( -. b e. B -> ( F " { b } ) =/= { Z } ) )
14 13 adantr 
 |-  ( ( b e. B /\ b e. dom F ) -> ( -. b e. B -> ( F " { b } ) =/= { Z } ) )
15 12 14 sylbi 
 |-  ( b e. ( B i^i dom F ) -> ( -. b e. B -> ( F " { b } ) =/= { Z } ) )
16 15 2 eleq2s 
 |-  ( b e. dom ( F |` B ) -> ( -. b e. B -> ( F " { b } ) =/= { Z } ) )
17 16 ad2antrl 
 |-  ( ( ( F e. V /\ Z e. W ) /\ ( b e. dom ( F |` B ) /\ ( ( F |` B ) " { b } ) =/= { Z } ) ) -> ( -. b e. B -> ( F " { b } ) =/= { Z } ) )
18 17 com12 
 |-  ( -. b e. B -> ( ( ( F e. V /\ Z e. W ) /\ ( b e. dom ( F |` B ) /\ ( ( F |` B ) " { b } ) =/= { Z } ) ) -> ( F " { b } ) =/= { Z } ) )
19 11 18 pm2.61i 
 |-  ( ( ( F e. V /\ Z e. W ) /\ ( b e. dom ( F |` B ) /\ ( ( F |` B ) " { b } ) =/= { Z } ) ) -> ( F " { b } ) =/= { Z } )
20 4 19 jca 
 |-  ( ( ( F e. V /\ Z e. W ) /\ ( b e. dom ( F |` B ) /\ ( ( F |` B ) " { b } ) =/= { Z } ) ) -> ( b e. dom F /\ ( F " { b } ) =/= { Z } ) )
21 20 ex 
 |-  ( ( F e. V /\ Z e. W ) -> ( ( b e. dom ( F |` B ) /\ ( ( F |` B ) " { b } ) =/= { Z } ) -> ( b e. dom F /\ ( F " { b } ) =/= { Z } ) ) )
22 21 ss2abdv 
 |-  ( ( F e. V /\ Z e. W ) -> { b | ( b e. dom ( F |` B ) /\ ( ( F |` B ) " { b } ) =/= { Z } ) } C_ { b | ( b e. dom F /\ ( F " { b } ) =/= { Z } ) } )
23 df-rab 
 |-  { b e. dom ( F |` B ) | ( ( F |` B ) " { b } ) =/= { Z } } = { b | ( b e. dom ( F |` B ) /\ ( ( F |` B ) " { b } ) =/= { Z } ) }
24 df-rab 
 |-  { b e. dom F | ( F " { b } ) =/= { Z } } = { b | ( b e. dom F /\ ( F " { b } ) =/= { Z } ) }
25 22 23 24 3sstr4g 
 |-  ( ( F e. V /\ Z e. W ) -> { b e. dom ( F |` B ) | ( ( F |` B ) " { b } ) =/= { Z } } C_ { b e. dom F | ( F " { b } ) =/= { Z } } )
26 resexg 
 |-  ( F e. V -> ( F |` B ) e. _V )
27 suppval 
 |-  ( ( ( F |` B ) e. _V /\ Z e. W ) -> ( ( F |` B ) supp Z ) = { b e. dom ( F |` B ) | ( ( F |` B ) " { b } ) =/= { Z } } )
28 26 27 sylan 
 |-  ( ( F e. V /\ Z e. W ) -> ( ( F |` B ) supp Z ) = { b e. dom ( F |` B ) | ( ( F |` B ) " { b } ) =/= { Z } } )
29 suppval 
 |-  ( ( F e. V /\ Z e. W ) -> ( F supp Z ) = { b e. dom F | ( F " { b } ) =/= { Z } } )
30 25 28 29 3sstr4d 
 |-  ( ( F e. V /\ Z e. W ) -> ( ( F |` B ) supp Z ) C_ ( F supp Z ) )