Metamath Proof Explorer

Theorem suppvalfn

Description: The value of the operation constructing the support of a function with a given domain. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by AV, 22-Apr-2019)

		Ref	Expression
	Assertion	suppvalfn	$⊢ (F Fn X \land X \in V \land Z \in W) \to F supp Z = \{i \in X \| F (i) \neq Z\}$

Proof

Step	Hyp	Ref	Expression
1		fnfun	$⊢ F Fn X \to Fun F$
2	1	3ad2ant1	$⊢ (F Fn X \land X \in V \land Z \in W) \to Fun F$
3		fnex	$⊢ (F Fn X \land X \in V) \to F \in V$
4	3	3adant3	$⊢ (F Fn X \land X \in V \land Z \in W) \to F \in V$
5		simp3	$⊢ (F Fn X \land X \in V \land Z \in W) \to Z \in W$
6		suppval1	$⊢ (Fun F \land F \in V \land Z \in W) \to F supp Z = \{i \in dom F \| F (i) \neq Z\}$
7	2 4 5 6	syl3anc	$⊢ (F Fn X \land X \in V \land Z \in W) \to F supp Z = \{i \in dom F \| F (i) \neq Z\}$
8		fndm	$⊢ F Fn X \to dom F = X$
9	8	3ad2ant1	$⊢ (F Fn X \land X \in V \land Z \in W) \to dom F = X$
10	9	rabeqdv	$⊢ (F Fn X \land X \in V \land Z \in W) \to \{i \in dom F \| F (i) \neq Z\} = \{i \in X \| F (i) \neq Z\}$
11	7 10	eqtrd	$⊢ (F Fn X \land X \in V \land Z \in W) \to F supp Z = \{i \in X \| F (i) \neq Z\}$