Metamath Proof Explorer

Theorem suppssrg

Description: A function is zero outside its support. Version of suppssr avoiding ax-rep by assuming F is a set rather than its domain A . (Contributed by SN, 5-May-2024)

		Ref	Expression
	Hypotheses	suppssrg.f	$⊢ φ \to F : A ⟶ B$
		suppssrg.n	$⊢ φ \to F supp Z \subseteq W$
		suppssrg.a	$⊢ φ \to F \in V$
		suppssrg.z	$⊢ φ \to Z \in U$
	Assertion	suppssrg	$⊢ (φ \land X \in (A ∖ W)) \to F (X) = Z$

Proof

Step	Hyp	Ref	Expression
1		suppssrg.f	$⊢ φ \to F : A ⟶ B$
2		suppssrg.n	$⊢ φ \to F supp Z \subseteq W$
3		suppssrg.a	$⊢ φ \to F \in V$
4		suppssrg.z	$⊢ φ \to Z \in U$
5		eldif	$⊢ X \in (A ∖ W) \leftrightarrow (X \in A \land \neg X \in W)$
6	1	ffnd	$⊢ φ \to F Fn A$
7		elsuppfng	$⊢ (F Fn A \land F \in V \land Z \in U) \to (X \in {supp}_{Z} (F) \leftrightarrow (X \in A \land F (X) \neq Z))$
8	6 3 4 7	syl3anc	$⊢ φ \to (X \in {supp}_{Z} (F) \leftrightarrow (X \in A \land F (X) \neq Z))$
9	2	sseld	$⊢ φ \to (X \in {supp}_{Z} (F) \to X \in W)$
10	8 9	sylbird	$⊢ φ \to ((X \in A \land F (X) \neq Z) \to X \in W)$
11	10	expdimp	$⊢ (φ \land X \in A) \to (F (X) \neq Z \to X \in W)$
12	11	necon1bd	$⊢ (φ \land X \in A) \to (\neg X \in W \to F (X) = Z)$
13	12	impr	$⊢ (φ \land (X \in A \land \neg X \in W)) \to F (X) = Z$
14	5 13	sylan2b	$⊢ (φ \land X \in (A ∖ W)) \to F (X) = Z$