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)

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 fdm ⊢ F : A ⟶ B → dom ⁡ F = A
6 dmexg ⊢ F ∈ V → dom ⁡ F ∈ V
7 6 adantr ⊢ F ∈ V ∧ Z ∈ V → dom ⁡ F ∈ V
8 eleq1 ⊢ A = dom ⁡ F → A ∈ V ↔ dom ⁡ F ∈ V
9 8 eqcoms ⊢ dom ⁡ F = A → A ∈ V ↔ dom ⁡ F ∈ V
10 7 9 syl5ibr ⊢ dom ⁡ F = A → F ∈ V ∧ Z ∈ V → A ∈ V
11 1 5 10 3syl ⊢ φ → F ∈ V ∧ Z ∈ V → A ∈ V
12 11 impcom ⊢ F ∈ V ∧ Z ∈ V ∧ φ → A ∈ V
13 simplr ⊢ F ∈ V ∧ Z ∈ V ∧ φ → Z ∈ V
14 elsuppfn ⊢ F Fn A ∧ A ∈ V ∧ Z ∈ V → k ∈ supp Z⁡ F ↔ k ∈ A ∧ F ⁡ k ≠ Z
15 4 12 13 14 syl3anc ⊢ F ∈ V ∧ Z ∈ V ∧ φ → k ∈ supp Z⁡ F ↔ k ∈ A ∧ F ⁡ k ≠ Z
16 eldif ⊢ k ∈ A ∖ W ↔ k ∈ A ∧ ¬ k ∈ W
17 2 adantll ⊢ F ∈ V ∧ Z ∈ V ∧ φ ∧ k ∈ A ∖ W → F ⁡ k = Z
18 16 17 sylan2br ⊢ F ∈ V ∧ Z ∈ V ∧ φ ∧ k ∈ A ∧ ¬ k ∈ W → F ⁡ k = Z
19 18 expr ⊢ F ∈ V ∧ Z ∈ V ∧ φ ∧ k ∈ A → ¬ k ∈ W → F ⁡ k = Z
20 19 necon1ad ⊢ F ∈ V ∧ Z ∈ V ∧ φ ∧ k ∈ A → F ⁡ k ≠ Z → k ∈ W
21 20 expimpd ⊢ F ∈ V ∧ Z ∈ V ∧ φ → k ∈ A ∧ F ⁡ k ≠ Z → k ∈ W
22 15 21 sylbid ⊢ F ∈ V ∧ Z ∈ V ∧ φ → k ∈ supp Z⁡ F → k ∈ W
23 22 ssrdv ⊢ F ∈ V ∧ Z ∈ V ∧ φ → F supp Z ⊆ W
24 23 ex ⊢ F ∈ V ∧ Z ∈ V → φ → F supp Z ⊆ W
25 supp0prc ⊢ ¬ F ∈ V ∧ Z ∈ V → F supp Z = ∅
26 0ss ⊢ ∅ ⊆ W
27 25 26 eqsstrdi ⊢ ¬ F ∈ V ∧ Z ∈ V → F supp Z ⊆ W
28 27 a1d ⊢ ¬ F ∈ V ∧ Z ∈ V → φ → F supp Z ⊆ W
29 24 28 pm2.61i ⊢ φ → F supp Z ⊆ W