Metamath Proof Explorer

Theorem ressuppssdif

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 ressuppssdif 
|- ( ( F e. V /\ Z e. W ) -> ( F supp Z ) C_ ( ( ( F |` B ) supp Z ) u. ( dom F \ B ) ) )

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( x e. ( { z e. dom F | ( F " { z } ) =/= { Z } } \ { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } ) <-> ( x e. { z e. dom F | ( F " { z } ) =/= { Z } } /\ -. x e. { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } ) )
2 sneq 
 |-  ( z = x -> { z } = { x } )
3 2 imaeq2d 
 |-  ( z = x -> ( F " { z } ) = ( F " { x } ) )
4 3 neeq1d 
 |-  ( z = x -> ( ( F " { z } ) =/= { Z } <-> ( F " { x } ) =/= { Z } ) )
5 4 elrab 
 |-  ( x e. { z e. dom F | ( F " { z } ) =/= { Z } } <-> ( x e. dom F /\ ( F " { x } ) =/= { Z } ) )
6 ianor 
 |-  ( -. ( x e. dom ( F |` B ) /\ ( ( F |` B ) " { x } ) =/= { Z } ) <-> ( -. x e. dom ( F |` B ) \/ -. ( ( F |` B ) " { x } ) =/= { Z } ) )
7 2 imaeq2d 
 |-  ( z = x -> ( ( F |` B ) " { z } ) = ( ( F |` B ) " { x } ) )
8 7 neeq1d 
 |-  ( z = x -> ( ( ( F |` B ) " { z } ) =/= { Z } <-> ( ( F |` B ) " { x } ) =/= { Z } ) )
9 8 elrab 
 |-  ( x e. { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } <-> ( x e. dom ( F |` B ) /\ ( ( F |` B ) " { x } ) =/= { Z } ) )
10 6 9 xchnxbir 
 |-  ( -. x e. { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } <-> ( -. x e. dom ( F |` B ) \/ -. ( ( F |` B ) " { x } ) =/= { Z } ) )
11 ianor 
 |-  ( -. ( x e. B /\ x e. dom F ) <-> ( -. x e. B \/ -. x e. dom F ) )
12 dmres 
 |-  dom ( F |` B ) = ( B i^i dom F )
13 12 elin2 
 |-  ( x e. dom ( F |` B ) <-> ( x e. B /\ x e. dom F ) )
14 11 13 xchnxbir 
 |-  ( -. x e. dom ( F |` B ) <-> ( -. x e. B \/ -. x e. dom F ) )
15 simpl 
 |-  ( ( x e. dom F /\ ( F " { x } ) =/= { Z } ) -> x e. dom F )
16 15 anim2i 
 |-  ( ( -. x e. B /\ ( x e. dom F /\ ( F " { x } ) =/= { Z } ) ) -> ( -. x e. B /\ x e. dom F ) )
17 16 ancomd 
 |-  ( ( -. x e. B /\ ( x e. dom F /\ ( F " { x } ) =/= { Z } ) ) -> ( x e. dom F /\ -. x e. B ) )
18 eldif 
 |-  ( x e. ( dom F \ B ) <-> ( x e. dom F /\ -. x e. B ) )
19 17 18 sylibr 
 |-  ( ( -. x e. B /\ ( x e. dom F /\ ( F " { x } ) =/= { Z } ) ) -> x e. ( dom F \ B ) )
20 19 ex 
 |-  ( -. x e. B -> ( ( x e. dom F /\ ( F " { x } ) =/= { Z } ) -> x e. ( dom F \ B ) ) )
21 pm2.24 
 |-  ( x e. dom F -> ( -. x e. dom F -> x e. ( dom F \ B ) ) )
22 21 adantr 
 |-  ( ( x e. dom F /\ ( F " { x } ) =/= { Z } ) -> ( -. x e. dom F -> x e. ( dom F \ B ) ) )
23 22 com12 
 |-  ( -. x e. dom F -> ( ( x e. dom F /\ ( F " { x } ) =/= { Z } ) -> x e. ( dom F \ B ) ) )
24 20 23 jaoi 
 |-  ( ( -. x e. B \/ -. x e. dom F ) -> ( ( x e. dom F /\ ( F " { x } ) =/= { Z } ) -> x e. ( dom F \ B ) ) )
25 14 24 sylbi 
 |-  ( -. x e. dom ( F |` B ) -> ( ( x e. dom F /\ ( F " { x } ) =/= { Z } ) -> x e. ( dom F \ B ) ) )
26 15 adantl 
 |-  ( ( -. ( ( F |` B ) " { x } ) =/= { Z } /\ ( x e. dom F /\ ( F " { x } ) =/= { Z } ) ) -> x e. dom F )
27 snssi 
 |-  ( x e. B -> { x } C_ B )
28 27 adantl 
 |-  ( ( x e. dom F /\ x e. B ) -> { x } C_ B )
29 resima2 
 |-  ( { x } C_ B -> ( ( F |` B ) " { x } ) = ( F " { x } ) )
30 28 29 syl 
 |-  ( ( x e. dom F /\ x e. B ) -> ( ( F |` B ) " { x } ) = ( F " { x } ) )
31 30 eqcomd 
 |-  ( ( x e. dom F /\ x e. B ) -> ( F " { x } ) = ( ( F |` B ) " { x } ) )
32 31 adantr 
 |-  ( ( ( x e. dom F /\ x e. B ) /\ ( ( F |` B ) " { x } ) = { Z } ) -> ( F " { x } ) = ( ( F |` B ) " { x } ) )
33 simpr 
 |-  ( ( ( x e. dom F /\ x e. B ) /\ ( ( F |` B ) " { x } ) = { Z } ) -> ( ( F |` B ) " { x } ) = { Z } )
34 32 33 eqtrd 
 |-  ( ( ( x e. dom F /\ x e. B ) /\ ( ( F |` B ) " { x } ) = { Z } ) -> ( F " { x } ) = { Z } )
35 34 ex 
 |-  ( ( x e. dom F /\ x e. B ) -> ( ( ( F |` B ) " { x } ) = { Z } -> ( F " { x } ) = { Z } ) )
36 35 necon3d 
 |-  ( ( x e. dom F /\ x e. B ) -> ( ( F " { x } ) =/= { Z } -> ( ( F |` B ) " { x } ) =/= { Z } ) )
37 36 impancom 
 |-  ( ( x e. dom F /\ ( F " { x } ) =/= { Z } ) -> ( x e. B -> ( ( F |` B ) " { x } ) =/= { Z } ) )
38 37 con3d 
 |-  ( ( x e. dom F /\ ( F " { x } ) =/= { Z } ) -> ( -. ( ( F |` B ) " { x } ) =/= { Z } -> -. x e. B ) )
39 38 impcom 
 |-  ( ( -. ( ( F |` B ) " { x } ) =/= { Z } /\ ( x e. dom F /\ ( F " { x } ) =/= { Z } ) ) -> -. x e. B )
40 26 39 eldifd 
 |-  ( ( -. ( ( F |` B ) " { x } ) =/= { Z } /\ ( x e. dom F /\ ( F " { x } ) =/= { Z } ) ) -> x e. ( dom F \ B ) )
41 40 ex 
 |-  ( -. ( ( F |` B ) " { x } ) =/= { Z } -> ( ( x e. dom F /\ ( F " { x } ) =/= { Z } ) -> x e. ( dom F \ B ) ) )
42 25 41 jaoi 
 |-  ( ( -. x e. dom ( F |` B ) \/ -. ( ( F |` B ) " { x } ) =/= { Z } ) -> ( ( x e. dom F /\ ( F " { x } ) =/= { Z } ) -> x e. ( dom F \ B ) ) )
43 42 impcom 
 |-  ( ( ( x e. dom F /\ ( F " { x } ) =/= { Z } ) /\ ( -. x e. dom ( F |` B ) \/ -. ( ( F |` B ) " { x } ) =/= { Z } ) ) -> x e. ( dom F \ B ) )
44 5 10 43 syl2anb 
 |-  ( ( x e. { z e. dom F | ( F " { z } ) =/= { Z } } /\ -. x e. { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } ) -> x e. ( dom F \ B ) )
45 1 44 sylbi 
 |-  ( x e. ( { z e. dom F | ( F " { z } ) =/= { Z } } \ { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } ) -> x e. ( dom F \ B ) )
46 45 a1i 
 |-  ( ( F e. V /\ Z e. W ) -> ( x e. ( { z e. dom F | ( F " { z } ) =/= { Z } } \ { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } ) -> x e. ( dom F \ B ) ) )
47 46 ssrdv 
 |-  ( ( F e. V /\ Z e. W ) -> ( { z e. dom F | ( F " { z } ) =/= { Z } } \ { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } ) C_ ( dom F \ B ) )
48 ssundif 
 |-  ( { z e. dom F | ( F " { z } ) =/= { Z } } C_ ( { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } u. ( dom F \ B ) ) <-> ( { z e. dom F | ( F " { z } ) =/= { Z } } \ { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } ) C_ ( dom F \ B ) )
49 47 48 sylibr 
 |-  ( ( F e. V /\ Z e. W ) -> { z e. dom F | ( F " { z } ) =/= { Z } } C_ ( { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } u. ( dom F \ B ) ) )
50 suppval 
 |-  ( ( F e. V /\ Z e. W ) -> ( F supp Z ) = { z e. dom F | ( F " { z } ) =/= { Z } } )
51 resexg 
 |-  ( F e. V -> ( F |` B ) e. _V )
52 suppval 
 |-  ( ( ( F |` B ) e. _V /\ Z e. W ) -> ( ( F |` B ) supp Z ) = { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } )
53 51 52 sylan 
 |-  ( ( F e. V /\ Z e. W ) -> ( ( F |` B ) supp Z ) = { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } )
54 53 uneq1d 
 |-  ( ( F e. V /\ Z e. W ) -> ( ( ( F |` B ) supp Z ) u. ( dom F \ B ) ) = ( { z e. dom ( F |` B ) | ( ( F |` B ) " { z } ) =/= { Z } } u. ( dom F \ B ) ) )
55 49 50 54 3sstr4d 
 |-  ( ( F e. V /\ Z e. W ) -> ( F supp Z ) C_ ( ( ( F |` B ) supp Z ) u. ( dom F \ B ) ) )