Metamath Proof Explorer

Theorem suppss

Description: Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 28-May-2019) (Proof shortened by SN, 5-Aug-2024)

Ref Expression
Hypotheses suppss.f ⊢ φ → F : A ⟶ B
suppss.n ⊢ φ ∧ k ∈ A ∖ W → F ⁡ k = Z
Assertion suppss ⊢ φ → F supp Z ⊆ W

Proof

Step Hyp Ref Expression
1 suppss.f ⊢ φ → F : A ⟶ B
2 suppss.n ⊢ φ ∧ k ∈ A ∖ W → F ⁡ k = Z
3 1 ffnd ⊢ φ → F Fn A
4 3 adantl ⊢ F ∈ V ∧ Z ∈ V ∧ φ → F Fn A
5 simpll ⊢ F ∈ V ∧ Z ∈ V ∧ φ → F ∈ V
6 simplr ⊢ F ∈ V ∧ Z ∈ V ∧ φ → Z ∈ V
7 elsuppfng ⊢ F Fn A ∧ F ∈ V ∧ Z ∈ V → k ∈ supp Z⁡ F ↔ k ∈ A ∧ F ⁡ k ≠ Z
8 4 5 6 7 syl3anc ⊢ F ∈ V ∧ Z ∈ V ∧ φ → k ∈ supp Z⁡ F ↔ k ∈ A ∧ F ⁡ k ≠ Z
9 eldif ⊢ k ∈ A ∖ W ↔ k ∈ A ∧ ¬ k ∈ W
10 2 adantll ⊢ F ∈ V ∧ Z ∈ V ∧ φ ∧ k ∈ A ∖ W → F ⁡ k = Z
11 9 10 sylan2br ⊢ F ∈ V ∧ Z ∈ V ∧ φ ∧ k ∈ A ∧ ¬ k ∈ W → F ⁡ k = Z
12 11 expr ⊢ F ∈ V ∧ Z ∈ V ∧ φ ∧ k ∈ A → ¬ k ∈ W → F ⁡ k = Z
13 12 necon1ad ⊢ F ∈ V ∧ Z ∈ V ∧ φ ∧ k ∈ A → F ⁡ k ≠ Z → k ∈ W
14 13 expimpd ⊢ F ∈ V ∧ Z ∈ V ∧ φ → k ∈ A ∧ F ⁡ k ≠ Z → k ∈ W
15 8 14 sylbid ⊢ F ∈ V ∧ Z ∈ V ∧ φ → k ∈ supp Z⁡ F → k ∈ W
16 15 ssrdv ⊢ F ∈ V ∧ Z ∈ V ∧ φ → F supp Z ⊆ W
17 16 ex ⊢ F ∈ V ∧ Z ∈ V → φ → F supp Z ⊆ W
18 supp0prc ⊢ ¬ F ∈ V ∧ Z ∈ V → F supp Z = ∅
19 0ss ⊢ ∅ ⊆ W
20 18 19 eqsstrdi ⊢ ¬ F ∈ V ∧ Z ∈ V → F supp Z ⊆ W
21 20 a1d ⊢ ¬ F ∈ V ∧ Z ∈ V → φ → F supp Z ⊆ W
22 17 21 pm2.61i ⊢ φ → F supp Z ⊆ W