Theorem fn0

Description: A function with empty domain is empty. (Contributed by NM, 15-Apr-1998) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Assertion	fn0	$$⊢FFn\varnothing \leftrightarrow F=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		fnrel	$$⊢FFn\varnothing \to \mathrm{Rel}F$$
2		fndm	$$⊢FFn\varnothing \to \mathrm{dom}F=\varnothing$$
3		reldm0	$$⊢\mathrm{Rel}F\to \left(F=\varnothing \leftrightarrow \mathrm{dom}F=\varnothing \right)$$
4	3	biimpar	$$⊢\left(\mathrm{Rel}F\wedge \mathrm{dom}F=\varnothing \right)\to F=\varnothing$$
5	1 2 4	syl2anc	$$⊢FFn\varnothing \to F=\varnothing$$
6		fun0	$$⊢\mathrm{Fun}\varnothing$$
7		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
8		df-fn	$$⊢\varnothing Fn\varnothing \leftrightarrow \left(\mathrm{Fun}\varnothing \wedge \mathrm{dom}\varnothing =\varnothing \right)$$
9	6 7 8	mpbir2an	$$⊢\varnothing Fn\varnothing$$
10		fneq1	$$⊢F=\varnothing \to \left(FFn\varnothing \leftrightarrow \varnothing Fn\varnothing \right)$$
11	9 10	mpbiri	$$⊢F=\varnothing \to FFn\varnothing$$
12	5 11	impbii	$$⊢FFn\varnothing \leftrightarrow F=\varnothing$$