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→ 𝐵 → ( 𝐹 “ 𝐴 ) = 𝐵 )