This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ { 𝐵 } )