Theorem fimadmfo

Description: A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022)

	Ref	Expression
Assertion	fimadmfo	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fdm	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
2		ffn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
3	2	adantr	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ dom 𝐹 = 𝐴 ) → 𝐹 Fn 𝐴 )
4		dffn4	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 )
5	3 4	sylib	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ dom 𝐹 = 𝐴 ) → 𝐹 : 𝐴 –onto→ ran 𝐹 )
6		imaeq2	⊢ ( 𝐴 = dom 𝐹 → ( 𝐹 “ 𝐴 ) = ( 𝐹 “ dom 𝐹 ) )
7		imadmrn	⊢ ( 𝐹 “ dom 𝐹 ) = ran 𝐹
8	6 7	eqtrdi	⊢ ( 𝐴 = dom 𝐹 → ( 𝐹 “ 𝐴 ) = ran 𝐹 )
9	8	eqcoms	⊢ ( dom 𝐹 = 𝐴 → ( 𝐹 “ 𝐴 ) = ran 𝐹 )
10	9	adantl	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ dom 𝐹 = 𝐴 ) → ( 𝐹 “ 𝐴 ) = ran 𝐹 )
11		foeq3	⊢ ( ( 𝐹 “ 𝐴 ) = ran 𝐹 → ( 𝐹 : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 ) )
12	10 11	syl	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ dom 𝐹 = 𝐴 ) → ( 𝐹 : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 ) )
13	5 12	mpbird	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ dom 𝐹 = 𝐴 ) → 𝐹 : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )
14	1 13	mpdan	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )