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	$⊢ φ \to F : A ⟶ B$
	suppss.n	$⊢ (φ \land k \in (A ∖ W)) \to F (k) = Z$
Assertion	suppss	$⊢ φ \to F supp Z \subseteq W$

Proof

Step	Hyp	Ref	Expression
1		suppss.f	$⊢ φ \to F : A ⟶ B$
2		suppss.n	$⊢ (φ \land k \in (A ∖ W)) \to F (k) = Z$
3	1	ffnd	$⊢ φ \to F Fn A$
4	3	adantl	$⊢ ((F \in V \land Z \in V) \land φ) \to F Fn A$
5		simpll	$⊢ ((F \in V \land Z \in V) \land φ) \to F \in V$
6		simplr	$⊢ ((F \in V \land Z \in V) \land φ) \to Z \in V$
7		elsuppfng	$⊢ (F Fn A \land F \in V \land Z \in V) \to (k \in {supp}_{Z} (F) \leftrightarrow (k \in A \land F (k) \neq Z))$
8	4 5 6 7	syl3anc	$⊢ ((F \in V \land Z \in V) \land φ) \to (k \in {supp}_{Z} (F) \leftrightarrow (k \in A \land F (k) \neq Z))$
9		eldif	$⊢ k \in (A ∖ W) \leftrightarrow (k \in A \land \neg k \in W)$
10	2	adantll	$⊢ (((F \in V \land Z \in V) \land φ) \land k \in (A ∖ W)) \to F (k) = Z$
11	9 10	sylan2br	$⊢ (((F \in V \land Z \in V) \land φ) \land (k \in A \land \neg k \in W)) \to F (k) = Z$
12	11	expr	$⊢ (((F \in V \land Z \in V) \land φ) \land k \in A) \to (\neg k \in W \to F (k) = Z)$
13	12	necon1ad	$⊢ (((F \in V \land Z \in V) \land φ) \land k \in A) \to (F (k) \neq Z \to k \in W)$
14	13	expimpd	$⊢ ((F \in V \land Z \in V) \land φ) \to ((k \in A \land F (k) \neq Z) \to k \in W)$
15	8 14	sylbid	$⊢ ((F \in V \land Z \in V) \land φ) \to (k \in {supp}_{Z} (F) \to k \in W)$
16	15	ssrdv	$⊢ ((F \in V \land Z \in V) \land φ) \to F supp Z \subseteq W$
17	16	ex	$⊢ (F \in V \land Z \in V) \to (φ \to F supp Z \subseteq W)$
18		supp0prc	$⊢ \neg (F \in V \land Z \in V) \to F supp Z = \emptyset$
19		0ss	$⊢ \emptyset \subseteq W$
20	18 19	eqsstrdi	$⊢ \neg (F \in V \land Z \in V) \to F supp Z \subseteq W$
21	20	a1d	$⊢ \neg (F \in V \land Z \in V) \to (φ \to F supp Z \subseteq W)$
22	17 21	pm2.61i	$⊢ φ \to F supp Z \subseteq W$

Metamath Proof Explorer

Theorem suppss

Proof