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 )