f00

Description: A class is a function with empty codomain iff it and its domain are empty. (Contributed by NM, 10-Dec-2003)

		Ref	Expression
	Assertion	f00	$⊢ F : A ⟶ \emptyset \leftrightarrow (F = \emptyset \land A = \emptyset)$

Step	Hyp	Ref	Expression
1		ffun	$⊢ F : A ⟶ \emptyset \to Fun F$
2		frn	$⊢ F : A ⟶ \emptyset \to ran F \subseteq \emptyset$
3		ss0	$⊢ ran F \subseteq \emptyset \to ran F = \emptyset$
4	2 3	syl	$⊢ F : A ⟶ \emptyset \to ran F = \emptyset$
5		dm0rn0	$⊢ dom F = \emptyset \leftrightarrow ran F = \emptyset$
6	4 5	sylibr	$⊢ F : A ⟶ \emptyset \to dom F = \emptyset$
7		df-fn	$⊢ F Fn \emptyset \leftrightarrow (Fun F \land dom F = \emptyset)$
8	1 6 7	sylanbrc	$⊢ F : A ⟶ \emptyset \to F Fn \emptyset$
9		fn0	$⊢ F Fn \emptyset \leftrightarrow F = \emptyset$
10	8 9	sylib	$⊢ F : A ⟶ \emptyset \to F = \emptyset$
11		fdm	$⊢ F : A ⟶ \emptyset \to dom F = A$
12	11 6	eqtr3d	$⊢ F : A ⟶ \emptyset \to A = \emptyset$
13	10 12	jca	$⊢ F : A ⟶ \emptyset \to (F = \emptyset \land A = \emptyset)$
14		f0	$⊢ \emptyset : \emptyset ⟶ \emptyset$
15		feq1	$⊢ F = \emptyset \to (F : A ⟶ \emptyset \leftrightarrow \emptyset : A ⟶ \emptyset)$
16		feq2	$⊢ A = \emptyset \to (\emptyset : A ⟶ \emptyset \leftrightarrow \emptyset : \emptyset ⟶ \emptyset)$
17	15 16	sylan9bb	$⊢ (F = \emptyset \land A = \emptyset) \to (F : A ⟶ \emptyset \leftrightarrow \emptyset : \emptyset ⟶ \emptyset)$
18	14 17	mpbiri	$⊢ (F = \emptyset \land A = \emptyset) \to F : A ⟶ \emptyset$
19	13 18	impbii	$⊢ F : A ⟶ \emptyset \leftrightarrow (F = \emptyset \land A = \emptyset)$

Metamath Proof Explorer