Metamath Proof Explorer


Theorem foima

Description: The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002)

Ref Expression
Assertion foima ( 𝐹 : 𝐴onto𝐵 → ( 𝐹𝐴 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 imadmrn ( 𝐹 “ dom 𝐹 ) = ran 𝐹
2 fof ( 𝐹 : 𝐴onto𝐵𝐹 : 𝐴𝐵 )
3 2 fdmd ( 𝐹 : 𝐴onto𝐵 → dom 𝐹 = 𝐴 )
4 3 imaeq2d ( 𝐹 : 𝐴onto𝐵 → ( 𝐹 “ dom 𝐹 ) = ( 𝐹𝐴 ) )
5 forn ( 𝐹 : 𝐴onto𝐵 → ran 𝐹 = 𝐵 )
6 1 4 5 3eqtr3a ( 𝐹 : 𝐴onto𝐵 → ( 𝐹𝐴 ) = 𝐵 )