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 ⟼ B supp Z ⊆ 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 ⟼ B supp Z = 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 ⟼ B supp Z ⊆ W
17 16 ex ⊢ Z ∈ V → φ → k ∈ A ⟼ B supp Z ⊆ 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 ⟼ B supp Z = ∅
21 19 20 syl ⊢ ¬ Z ∈ V → k ∈ A ⟼ B supp Z = ∅
22 0ss ⊢ ∅ ⊆ W
23 21 22 eqsstrdi ⊢ ¬ Z ∈ V → k ∈ A ⟼ B supp Z ⊆ W
24 23 a1d ⊢ ¬ Z ∈ V → φ → k ∈ A ⟼ B supp Z ⊆ W
25 17 24 pm2.61i ⊢ φ → k ∈ A ⟼ B supp Z ⊆ W