f0rn0

Description: If there is no element in the range of a function, its domain must be empty. (Contributed by Alexander van der Vekens, 12-Jul-2018)

		Ref	Expression
	Assertion	f0rn0	$⊢ (E : X ⟶ Y \land \neg \exists y \in Y y \in ran E) \to X = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		fdm	$⊢ E : X ⟶ Y \to dom E = X$
2		frn	$⊢ E : X ⟶ Y \to ran E \subseteq Y$
3		ralnex	$⊢ \forall y \in Y \neg y \in ran E \leftrightarrow \neg \exists y \in Y y \in ran E$
4		disj	$⊢ Y \cap ran E = \emptyset \leftrightarrow \forall y \in Y \neg y \in ran E$
5		df-ss	$⊢ ran E \subseteq Y \leftrightarrow ran E \cap Y = ran E$
6		incom	$⊢ ran E \cap Y = Y \cap ran E$
7	6	eqeq1i	$⊢ ran E \cap Y = ran E \leftrightarrow Y \cap ran E = ran E$
8		eqtr2	$⊢ (Y \cap ran E = ran E \land Y \cap ran E = \emptyset) \to ran E = \emptyset$
9	8	ex	$⊢ Y \cap ran E = ran E \to (Y \cap ran E = \emptyset \to ran E = \emptyset)$
10	7 9	sylbi	$⊢ ran E \cap Y = ran E \to (Y \cap ran E = \emptyset \to ran E = \emptyset)$
11	5 10	sylbi	$⊢ ran E \subseteq Y \to (Y \cap ran E = \emptyset \to ran E = \emptyset)$
12	4 11	syl5bir	$⊢ ran E \subseteq Y \to (\forall y \in Y \neg y \in ran E \to ran E = \emptyset)$
13	3 12	syl5bir	$⊢ ran E \subseteq Y \to (\neg \exists y \in Y y \in ran E \to ran E = \emptyset)$
14	2 13	syl	$⊢ E : X ⟶ Y \to (\neg \exists y \in Y y \in ran E \to ran E = \emptyset)$
15	14	imp	$⊢ (E : X ⟶ Y \land \neg \exists y \in Y y \in ran E) \to ran E = \emptyset$
16	15	adantl	$⊢ (dom E = X \land (E : X ⟶ Y \land \neg \exists y \in Y y \in ran E)) \to ran E = \emptyset$
17		dm0rn0	$⊢ dom E = \emptyset \leftrightarrow ran E = \emptyset$
18	16 17	sylibr	$⊢ (dom E = X \land (E : X ⟶ Y \land \neg \exists y \in Y y \in ran E)) \to dom E = \emptyset$
19		eqeq1	$⊢ X = dom E \to (X = \emptyset \leftrightarrow dom E = \emptyset)$
20	19	eqcoms	$⊢ dom E = X \to (X = \emptyset \leftrightarrow dom E = \emptyset)$
21	20	adantr	$⊢ (dom E = X \land (E : X ⟶ Y \land \neg \exists y \in Y y \in ran E)) \to (X = \emptyset \leftrightarrow dom E = \emptyset)$
22	18 21	mpbird	$⊢ (dom E = X \land (E : X ⟶ Y \land \neg \exists y \in Y y \in ran E)) \to X = \emptyset$
23	22	exp32	$⊢ dom E = X \to (E : X ⟶ Y \to (\neg \exists y \in Y y \in ran E \to X = \emptyset))$
24	1 23	mpcom	$⊢ E : X ⟶ Y \to (\neg \exists y \in Y y \in ran E \to X = \emptyset)$
25	24	imp	$⊢ (E : X ⟶ Y \land \neg \exists y \in Y y \in ran E) \to X = \emptyset$

Metamath Proof Explorer

Theorem f0rn0

Proof