fdomne0

Description: A function with non-empty domain is non-empty and has non-empty codomain. (Contributed by Zhi Wang, 1-Oct-2024)

		Ref	Expression
	Assertion	fdomne0	$⊢ (F : X ⟶ Y \land X \neq \emptyset) \to (F \neq \emptyset \land Y \neq \emptyset)$

Step	Hyp	Ref	Expression
1		f0dom0	$⊢ F : X ⟶ Y \to (X = \emptyset \leftrightarrow F = \emptyset)$
2	1	necon3bid	$⊢ F : X ⟶ Y \to (X \neq \emptyset \leftrightarrow F \neq \emptyset)$
3	2	biimpa	$⊢ (F : X ⟶ Y \land X \neq \emptyset) \to F \neq \emptyset$
4		feq3	$⊢ Y = \emptyset \to (F : X ⟶ Y \leftrightarrow F : X ⟶ \emptyset)$
5		f00	$⊢ F : X ⟶ \emptyset \leftrightarrow (F = \emptyset \land X = \emptyset)$
6	5	simprbi	$⊢ F : X ⟶ \emptyset \to X = \emptyset$
7	4 6	biimtrdi	$⊢ Y = \emptyset \to (F : X ⟶ Y \to X = \emptyset)$
8		nne	$⊢ \neg X \neq \emptyset \leftrightarrow X = \emptyset$
9	7 8	imbitrrdi	$⊢ Y = \emptyset \to (F : X ⟶ Y \to \neg X \neq \emptyset)$
10		imnan	$⊢ (F : X ⟶ Y \to \neg X \neq \emptyset) \leftrightarrow \neg (F : X ⟶ Y \land X \neq \emptyset)$
11	9 10	sylib	$⊢ Y = \emptyset \to \neg (F : X ⟶ Y \land X \neq \emptyset)$
12	11	necon2ai	$⊢ (F : X ⟶ Y \land X \neq \emptyset) \to Y \neq \emptyset$
13	3 12	jca	$⊢ (F : X ⟶ Y \land X \neq \emptyset) \to (F \neq \emptyset \land Y \neq \emptyset)$

Metamath Proof Explorer