This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem suppss2

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

Ref Expression
Hypotheses suppss2.n 
|- ( ( ph /\ k e. ( A \ W ) ) -> B = Z )
suppss2.a 
|- ( ph -> A e. V )
Assertion suppss2 
|- ( ph -> ( ( k e. A |-> B ) supp Z ) C_ W )

Proof

Step Hyp Ref Expression
1 suppss2.n 
 |-  ( ( ph /\ k e. ( A \ W ) ) -> B = Z )
2 suppss2.a 
 |-  ( ph -> A e. V )
3 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
4 2 adantl 
 |-  ( ( Z e. _V /\ ph ) -> A e. V )
5 simpl 
 |-  ( ( Z e. _V /\ ph ) -> Z e. _V )
6 3 4 5 mptsuppdifd 
 |-  ( ( Z e. _V /\ ph ) -> ( ( k e. A |-> B ) supp Z ) = { k e. A | B e. ( _V \ { Z } ) } )
7 eldifsni 
 |-  ( B e. ( _V \ { Z } ) -> B =/= Z )
8 eldif 
 |-  ( k e. ( A \ W ) <-> ( k e. A /\ -. k e. W ) )
9 1 adantll 
 |-  ( ( ( Z e. _V /\ ph ) /\ k e. ( A \ W ) ) -> B = Z )
10 8 9 sylan2br 
 |-  ( ( ( Z e. _V /\ ph ) /\ ( k e. A /\ -. k e. W ) ) -> B = Z )
11 10 expr 
 |-  ( ( ( Z e. _V /\ ph ) /\ k e. A ) -> ( -. k e. W -> B = Z ) )
12 11 necon1ad 
 |-  ( ( ( Z e. _V /\ ph ) /\ k e. A ) -> ( B =/= Z -> k e. W ) )
13 7 12 syl5 
 |-  ( ( ( Z e. _V /\ ph ) /\ k e. A ) -> ( B e. ( _V \ { Z } ) -> k e. W ) )
14 13 3impia 
 |-  ( ( ( Z e. _V /\ ph ) /\ k e. A /\ B e. ( _V \ { Z } ) ) -> k e. W )
15 14 rabssdv 
 |-  ( ( Z e. _V /\ ph ) -> { k e. A | B e. ( _V \ { Z } ) } C_ W )
16 6 15 eqsstrd 
 |-  ( ( Z e. _V /\ ph ) -> ( ( k e. A |-> B ) supp Z ) C_ W )
17 16 ex 
 |-  ( Z e. _V -> ( ph -> ( ( k e. A |-> B ) supp Z ) C_ W ) )
18 id 
 |-  ( -. Z e. _V -> -. Z e. _V )
19 18 intnand 
 |-  ( -. Z e. _V -> -. ( ( k e. A |-> B ) e. _V /\ Z e. _V ) )
20 supp0prc 
 |-  ( -. ( ( k e. A |-> B ) e. _V /\ Z e. _V ) -> ( ( k e. A |-> B ) supp Z ) = (/) )
21 19 20 syl 
 |-  ( -. Z e. _V -> ( ( k e. A |-> B ) supp Z ) = (/) )
22 0ss 
 |-  (/) C_ W
23 21 22 eqsstrdi 
 |-  ( -. Z e. _V -> ( ( k e. A |-> B ) supp Z ) C_ W )
24 23 a1d 
 |-  ( -. Z e. _V -> ( ph -> ( ( k e. A |-> B ) supp Z ) C_ W ) )
25 17 24 pm2.61i 
 |-  ( ph -> ( ( k e. A |-> B ) supp Z ) C_ W )