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

Metamath Proof Explorer

Theorem fofn

Description: An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008)

Ref Expression
Assertion fofn ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 )

Proof

Step Hyp Ref Expression
1 fof ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 1 ffnd ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 )