Metamath Proof Explorer


Theorem suppssOLD

Description: Obsolete version of suppss as of 5-Aug-2024. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 28-May-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses suppss.f
|- ( ph -> F : A --> B )
suppss.n
|- ( ( ph /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )
Assertion suppssOLD
|- ( 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 )
4 3 adantl
 |-  ( ( ( 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 )
7 6 adantr
 |-  ( ( 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 ) )
17 2 adantll
 |-  ( ( ( ( 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 ) )
20 19 necon1ad
 |-  ( ( ( ( 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 )