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 ⊢φ∧k∈A∖W→B=Z
suppss2.a ⊢φ→A∈V
Assertion suppss2 ⊢φ→k∈A⟼BsuppZ⊆W

Proof

Step Hyp Ref Expression
1 suppss2.n ⊢φ∧k∈A∖W→B=Z
2 suppss2.a ⊢φ→A∈V
3 eqid ⊢k∈A⟼B=k∈A⟼B
4 2 adantl ⊢Z∈V∧φ→A∈V
5 simpl ⊢Z∈V∧φ→Z∈V
6 3 4 5 mptsuppdifd ⊢Z∈V∧φ→k∈A⟼BsuppZ=k∈A|B∈V∖Z
7 eldifsni ⊢B∈V∖Z→B≠Z
8 eldif ⊢k∈A∖W↔k∈A∧¬k∈W
9 1 adantll ⊢Z∈V∧φ∧k∈A∖W→B=Z
10 8 9 sylan2br ⊢Z∈V∧φ∧k∈A∧¬k∈W→B=Z
11 10 expr ⊢Z∈V∧φ∧k∈A→¬k∈W→B=Z
12 11 necon1ad ⊢Z∈V∧φ∧k∈A→B≠Z→k∈W
13 7 12 syl5 ⊢Z∈V∧φ∧k∈A→B∈V∖Z→k∈W
14 13 3impia ⊢Z∈V∧φ∧k∈A∧B∈V∖Z→k∈W
15 14 rabssdv ⊢Z∈V∧φ→k∈A|B∈V∖Z⊆W
16 6 15 eqsstrd ⊢Z∈V∧φ→k∈A⟼BsuppZ⊆W
17 16 ex ⊢Z∈V→φ→k∈A⟼BsuppZ⊆W
18 id ⊢¬Z∈V→¬Z∈V
19 18 intnand ⊢¬Z∈V→¬k∈A⟼B∈V∧Z∈V
20 supp0prc ⊢¬k∈A⟼B∈V∧Z∈V→k∈A⟼BsuppZ=∅
21 19 20 syl ⊢¬Z∈V→k∈A⟼BsuppZ=∅
22 0ss ⊢∅⊆W
23 21 22 eqsstrdi ⊢¬Z∈V→k∈A⟼BsuppZ⊆W
24 23 a1d ⊢¬Z∈V→φ→k∈A⟼BsuppZ⊆W
25 17 24 pm2.61i ⊢φ→k∈A⟼BsuppZ⊆W