# 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 ( ( 𝜑𝑘 ∈ ( 𝐴𝑊 ) ) → 𝐵 = 𝑍 )
suppss2.a ( 𝜑𝐴𝑉 )
Assertion suppss2 ( 𝜑 → ( ( 𝑘𝐴𝐵 ) supp 𝑍 ) ⊆ 𝑊 )

### Proof

Step Hyp Ref Expression
1 suppss2.n ( ( 𝜑𝑘 ∈ ( 𝐴𝑊 ) ) → 𝐵 = 𝑍 )
2 suppss2.a ( 𝜑𝐴𝑉 )
3 eqid ( 𝑘𝐴𝐵 ) = ( 𝑘𝐴𝐵 )
4 2 adantl ( ( 𝑍 ∈ V ∧ 𝜑 ) → 𝐴𝑉 )
5 simpl ( ( 𝑍 ∈ V ∧ 𝜑 ) → 𝑍 ∈ V )
6 3 4 5 mptsuppdifd ( ( 𝑍 ∈ V ∧ 𝜑 ) → ( ( 𝑘𝐴𝐵 ) supp 𝑍 ) = { 𝑘𝐴𝐵 ∈ ( V ∖ { 𝑍 } ) } )
7 eldifsni ( 𝐵 ∈ ( V ∖ { 𝑍 } ) → 𝐵𝑍 )
8 eldif ( 𝑘 ∈ ( 𝐴𝑊 ) ↔ ( 𝑘𝐴 ∧ ¬ 𝑘𝑊 ) )
9 1 adantll ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝐴𝑊 ) ) → 𝐵 = 𝑍 )
10 8 9 sylan2br ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ ( 𝑘𝐴 ∧ ¬ 𝑘𝑊 ) ) → 𝐵 = 𝑍 )
11 10 expr ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑘𝐴 ) → ( ¬ 𝑘𝑊𝐵 = 𝑍 ) )
12 11 necon1ad ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑘𝐴 ) → ( 𝐵𝑍𝑘𝑊 ) )
13 7 12 syl5 ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑘𝐴 ) → ( 𝐵 ∈ ( V ∖ { 𝑍 } ) → 𝑘𝑊 ) )
14 13 3impia ( ( ( 𝑍 ∈ V ∧ 𝜑 ) ∧ 𝑘𝐴𝐵 ∈ ( V ∖ { 𝑍 } ) ) → 𝑘𝑊 )
15 14 rabssdv ( ( 𝑍 ∈ V ∧ 𝜑 ) → { 𝑘𝐴𝐵 ∈ ( V ∖ { 𝑍 } ) } ⊆ 𝑊 )
16 6 15 eqsstrd ( ( 𝑍 ∈ V ∧ 𝜑 ) → ( ( 𝑘𝐴𝐵 ) supp 𝑍 ) ⊆ 𝑊 )
17 16 ex ( 𝑍 ∈ V → ( 𝜑 → ( ( 𝑘𝐴𝐵 ) supp 𝑍 ) ⊆ 𝑊 ) )
18 id ( ¬ 𝑍 ∈ V → ¬ 𝑍 ∈ V )
19 18 intnand ( ¬ 𝑍 ∈ V → ¬ ( ( 𝑘𝐴𝐵 ) ∈ V ∧ 𝑍 ∈ V ) )
20 supp0prc ( ¬ ( ( 𝑘𝐴𝐵 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑘𝐴𝐵 ) supp 𝑍 ) = ∅ )
21 19 20 syl ( ¬ 𝑍 ∈ V → ( ( 𝑘𝐴𝐵 ) supp 𝑍 ) = ∅ )
22 0ss ∅ ⊆ 𝑊
23 21 22 eqsstrdi ( ¬ 𝑍 ∈ V → ( ( 𝑘𝐴𝐵 ) supp 𝑍 ) ⊆ 𝑊 )
24 23 a1d ( ¬ 𝑍 ∈ V → ( 𝜑 → ( ( 𝑘𝐴𝐵 ) supp 𝑍 ) ⊆ 𝑊 ) )
25 17 24 pm2.61i ( 𝜑 → ( ( 𝑘𝐴𝐵 ) supp 𝑍 ) ⊆ 𝑊 )