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

Metamath Proof Explorer

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