Description: An onto mapping is a function. (Contributed by NM, 29-Mar-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | fofun | ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → Fun 𝐹 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fof | ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 ) | |
2 | 1 | ffund | ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → Fun 𝐹 ) |