Theorem fo00

Description: Onto mapping of the empty set. (Contributed by NM, 22-Mar-2006)

	Ref	Expression
Assertion	fo00	$$⊢F:\varnothing \underset{onto}{⟶}A\leftrightarrow \left(F=\varnothing \wedge A=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		fofn	$$⊢F:\varnothing \underset{onto}{⟶}A\to FFn\varnothing$$
2		fn0	$$⊢FFn\varnothing \leftrightarrow F=\varnothing$$
3		f10	$$⊢\varnothing :\varnothing \underset{1-1}{⟶}A$$
4		f1eq1	$$⊢F=\varnothing \to \left(F:\varnothing \underset{1-1}{⟶}A\leftrightarrow \varnothing :\varnothing \underset{1-1}{⟶}A\right)$$
5	3 4	mpbiri	$$⊢F=\varnothing \to F:\varnothing \underset{1-1}{⟶}A$$
6	2 5	sylbi	$$⊢FFn\varnothing \to F:\varnothing \underset{1-1}{⟶}A$$
7	1 6	syl	$$⊢F:\varnothing \underset{onto}{⟶}A\to F:\varnothing \underset{1-1}{⟶}A$$
8	7	ancri	$$⊢F:\varnothing \underset{onto}{⟶}A\to \left(F:\varnothing \underset{1-1}{⟶}A\wedge F:\varnothing \underset{onto}{⟶}A\right)$$
9		df-f1o	$$⊢F:\varnothing \underset{1-1\; onto}{⟶}A\leftrightarrow \left(F:\varnothing \underset{1-1}{⟶}A\wedge F:\varnothing \underset{onto}{⟶}A\right)$$
10	8 9	sylibr	$$⊢F:\varnothing \underset{onto}{⟶}A\to F:\varnothing \underset{1-1\; onto}{⟶}A$$
11		f1ofo	$$⊢F:\varnothing \underset{1-1\; onto}{⟶}A\to F:\varnothing \underset{onto}{⟶}A$$
12	10 11	impbii	$$⊢F:\varnothing \underset{onto}{⟶}A\leftrightarrow F:\varnothing \underset{1-1\; onto}{⟶}A$$
13		f1o00	$$⊢F:\varnothing \underset{1-1\; onto}{⟶}A\leftrightarrow \left(F=\varnothing \wedge A=\varnothing \right)$$
14	12 13	bitri	$$⊢F:\varnothing \underset{onto}{⟶}A\leftrightarrow \left(F=\varnothing \wedge A=\varnothing \right)$$