foconst

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

		Ref	Expression
	Assertion	foconst	$⊢ (F : A ⟶ \{B\} \land F \neq \emptyset) \to F : A \underset{onto}{⟶} \{B\}$

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

Metamath Proof Explorer