# Metamath Proof Explorer

## Theorem suppss

Description: Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 28-May-2019)

Ref Expression
Hypotheses suppss.f
`|- ( ph -> F : A --> B )`
suppss.n
`|- ( ( ph /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )`
Assertion suppss
`|- ( ph -> ( F supp Z ) C_ W )`

### Proof

Step Hyp Ref Expression
1 suppss.f
` |-  ( ph -> F : A --> B )`
2 suppss.n
` |-  ( ( ph /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )`
3 1 ffnd
` |-  ( ph -> F Fn A )`
` |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> F Fn A )`
5 fdm
` |-  ( F : A --> B -> dom F = A )`
6 dmexg
` |-  ( F e. _V -> dom F e. _V )`
` |-  ( ( F e. _V /\ Z e. _V ) -> dom F e. _V )`
8 eleq1
` |-  ( A = dom F -> ( A e. _V <-> dom F e. _V ) )`
9 8 eqcoms
` |-  ( dom F = A -> ( A e. _V <-> dom F e. _V ) )`
10 7 9 syl5ibr
` |-  ( dom F = A -> ( ( F e. _V /\ Z e. _V ) -> A e. _V ) )`
11 1 5 10 3syl
` |-  ( ph -> ( ( F e. _V /\ Z e. _V ) -> A e. _V ) )`
12 11 impcom
` |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> A e. _V )`
13 simplr
` |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> Z e. _V )`
14 elsuppfn
` |-  ( ( F Fn A /\ A e. _V /\ Z e. _V ) -> ( k e. ( F supp Z ) <-> ( k e. A /\ ( F ` k ) =/= Z ) ) )`
15 4 12 13 14 syl3anc
` |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( k e. ( F supp Z ) <-> ( k e. A /\ ( F ` k ) =/= Z ) ) )`
16 eldif
` |-  ( k e. ( A \ W ) <-> ( k e. A /\ -. k e. W ) )`
` |-  ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )`
18 16 17 sylan2br
` |-  ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ ( k e. A /\ -. k e. W ) ) -> ( F ` k ) = Z )`
19 18 expr
` |-  ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ k e. A ) -> ( -. k e. W -> ( F ` k ) = Z ) )`
` |-  ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ k e. A ) -> ( ( F ` k ) =/= Z -> k e. W ) )`
21 20 expimpd
` |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( ( k e. A /\ ( F ` k ) =/= Z ) -> k e. W ) )`
22 15 21 sylbid
` |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( k e. ( F supp Z ) -> k e. W ) )`
23 22 ssrdv
` |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( F supp Z ) C_ W )`
24 23 ex
` |-  ( ( F e. _V /\ Z e. _V ) -> ( ph -> ( F supp Z ) C_ W ) )`
25 supp0prc
` |-  ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) = (/) )`
26 0ss
` |-  (/) C_ W`
27 25 26 eqsstrdi
` |-  ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) C_ W )`
28 27 a1d
` |-  ( -. ( F e. _V /\ Z e. _V ) -> ( ph -> ( F supp Z ) C_ W ) )`
29 24 28 pm2.61i
` |-  ( ph -> ( F supp Z ) C_ W )`