Metamath Proof Explorer

Theorem suppdm

Description: If the range of a function does not contain the zero, the support of the function equals its domain. (Contributed by AV, 20-May-2020)

		Ref	Expression
	Assertion	suppdm	$⊢ ((Fun F \land F \in V \land Z \in W) \land Z \notin ran F) \to F supp Z = dom F$

Proof

Step	Hyp	Ref	Expression
1		suppval1	$⊢ (Fun F \land F \in V \land Z \in W) \to F supp Z = \{x \in dom F \| F (x) \neq Z\}$
2	1	adantr	$⊢ ((Fun F \land F \in V \land Z \in W) \land Z \notin ran F) \to F supp Z = \{x \in dom F \| F (x) \neq Z\}$
3		df-nel	$⊢ Z \notin ran F \leftrightarrow \neg Z \in ran F$
4		fvelrn	$⊢ (Fun F \land x \in dom F) \to F (x) \in ran F$
5	4	3ad2antl1	$⊢ ((Fun F \land F \in V \land Z \in W) \land x \in dom F) \to F (x) \in ran F$
6		eleq1	$⊢ Z = F (x) \to (Z \in ran F \leftrightarrow F (x) \in ran F)$
7	6	eqcoms	$⊢ F (x) = Z \to (Z \in ran F \leftrightarrow F (x) \in ran F)$
8	5 7	syl5ibrcom	$⊢ ((Fun F \land F \in V \land Z \in W) \land x \in dom F) \to (F (x) = Z \to Z \in ran F)$
9	8	necon3bd	$⊢ ((Fun F \land F \in V \land Z \in W) \land x \in dom F) \to (\neg Z \in ran F \to F (x) \neq Z)$
10	3 9	biimtrid	$⊢ ((Fun F \land F \in V \land Z \in W) \land x \in dom F) \to (Z \notin ran F \to F (x) \neq Z)$
11	10	impancom	$⊢ ((Fun F \land F \in V \land Z \in W) \land Z \notin ran F) \to (x \in dom F \to F (x) \neq Z)$
12	11	ralrimiv	$⊢ ((Fun F \land F \in V \land Z \in W) \land Z \notin ran F) \to \forall x \in dom F F (x) \neq Z$
13		rabid2	$⊢ dom F = \{x \in dom F \| F (x) \neq Z\} \leftrightarrow \forall x \in dom F F (x) \neq Z$
14	12 13	sylibr	$⊢ ((Fun F \land F \in V \land Z \in W) \land Z \notin ran F) \to dom F = \{x \in dom F \| F (x) \neq Z\}$
15	2 14	eqtr4d	$⊢ ((Fun F \land F \in V \land Z \in W) \land Z \notin ran F) \to F supp Z = dom F$