Theorem foconst

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

	Ref	Expression
Assertion	foconst	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐹 ≠ ∅ ) → 𝐹 : 𝐴 –onto→ { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		frel	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } → Rel 𝐹 )
2		relrn0	⊢ ( Rel 𝐹 → ( 𝐹 = ∅ ↔ ran 𝐹 = ∅ ) )
3	2	necon3abid	⊢ ( Rel 𝐹 → ( 𝐹 ≠ ∅ ↔ ¬ ran 𝐹 = ∅ ) )
4	1 3	syl	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } → ( 𝐹 ≠ ∅ ↔ ¬ ran 𝐹 = ∅ ) )
5		frn	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } → ran 𝐹 ⊆ { 𝐵 } )
6		sssn	⊢ ( ran 𝐹 ⊆ { 𝐵 } ↔ ( ran 𝐹 = ∅ ∨ ran 𝐹 = { 𝐵 } ) )
7	5 6	sylib	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } → ( ran 𝐹 = ∅ ∨ ran 𝐹 = { 𝐵 } ) )
8	7	ord	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } → ( ¬ ran 𝐹 = ∅ → ran 𝐹 = { 𝐵 } ) )
9	4 8	sylbid	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } → ( 𝐹 ≠ ∅ → ran 𝐹 = { 𝐵 } ) )
10	9	imdistani	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐹 ≠ ∅ ) → ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ran 𝐹 = { 𝐵 } ) )
11		dffo2	⊢ ( 𝐹 : 𝐴 –onto→ { 𝐵 } ↔ ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ ran 𝐹 = { 𝐵 } ) )
12	10 11	sylibr	⊢ ( ( 𝐹 : 𝐴 ⟶ { 𝐵 } ∧ 𝐹 ≠ ∅ ) → 𝐹 : 𝐴 –onto→ { 𝐵 } )