Theorem foconst

Description: A nonzero constant function is onto. (Contributed by NM, 12-Jan-2007)

	Ref	Expression
Assertion	foconst	$$⊢\left(F:A⟶\left\{B\right\}\wedge F\ne \varnothing \right)\to F:A\underset{onto}{⟶}\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		frel	$$⊢F:A⟶\left\{B\right\}\to \mathrm{Rel}F$$
2		relrn0	$$⊢\mathrm{Rel}F\to \left(F=\varnothing \leftrightarrow \mathrm{ran}F=\varnothing \right)$$
3	2	necon3abid	$$⊢\mathrm{Rel}F\to \left(F\ne \varnothing \leftrightarrow \neg \mathrm{ran}F=\varnothing \right)$$
4	1 3	syl	$$⊢F:A⟶\left\{B\right\}\to \left(F\ne \varnothing \leftrightarrow \neg \mathrm{ran}F=\varnothing \right)$$
5		frn	$$⊢F:A⟶\left\{B\right\}\to \mathrm{ran}F\subseteq \left\{B\right\}$$
6		sssn	$$⊢\mathrm{ran}F\subseteq \left\{B\right\}\leftrightarrow \left(\mathrm{ran}F=\varnothing \vee \mathrm{ran}F=\left\{B\right\}\right)$$
7	5 6	sylib	$$⊢F:A⟶\left\{B\right\}\to \left(\mathrm{ran}F=\varnothing \vee \mathrm{ran}F=\left\{B\right\}\right)$$
8	7	ord	$$⊢F:A⟶\left\{B\right\}\to \left(\neg \mathrm{ran}F=\varnothing \to \mathrm{ran}F=\left\{B\right\}\right)$$
9	4 8	sylbid	$$⊢F:A⟶\left\{B\right\}\to \left(F\ne \varnothing \to \mathrm{ran}F=\left\{B\right\}\right)$$
10	9	imdistani	$$⊢\left(F:A⟶\left\{B\right\}\wedge F\ne \varnothing \right)\to \left(F:A⟶\left\{B\right\}\wedge \mathrm{ran}F=\left\{B\right\}\right)$$
11		dffo2	$$⊢F:A\underset{onto}{⟶}\left\{B\right\}\leftrightarrow \left(F:A⟶\left\{B\right\}\wedge \mathrm{ran}F=\left\{B\right\}\right)$$
12	10 11	sylibr	$$⊢\left(F:A⟶\left\{B\right\}\wedge F\ne \varnothing \right)\to F:A\underset{onto}{⟶}\left\{B\right\}$$