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

Metamath Proof Explorer

Theorem fimadmfoALT

Description: Alternate proof of fimadmfo , based on fores . A function is a function onto the image of its domain. (Contributed by AV, 1-Dec-2022) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 fdm ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
2 frel ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Rel 𝐹 )
3 resdm ⊢ ( Rel 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
4 3 eqcomd ⊢ ( Rel 𝐹 → 𝐹 = ( 𝐹 ↾ dom 𝐹 ) )
5 2 4 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 = ( 𝐹 ↾ dom 𝐹 ) )
6 reseq2 ⊢ ( dom 𝐹 = 𝐴 → ( 𝐹 ↾ dom 𝐹 ) = ( 𝐹 ↾ 𝐴 ) )
7 5 6 sylan9eq ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ dom 𝐹 = 𝐴 ) → 𝐹 = ( 𝐹 ↾ 𝐴 ) )
8 1 7 mpdan ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 = ( 𝐹 ↾ 𝐴 ) )
9 ffun ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Fun 𝐹 )
10 eqimss2 ⊢ ( dom 𝐹 = 𝐴 → 𝐴 ⊆ dom 𝐹 )
11 1 10 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐴 ⊆ dom 𝐹 )
12 9 11 jca ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) )
13 12 adantr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐹 = ( 𝐹 ↾ 𝐴 ) ) → ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) )
14 fores ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )
15 13 14 syl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐹 = ( 𝐹 ↾ 𝐴 ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )
16 foeq1 ⊢ ( 𝐹 = ( 𝐹 ↾ 𝐴 ) → ( 𝐹 : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ) )
17 16 adantl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐹 = ( 𝐹 ↾ 𝐴 ) ) → ( 𝐹 : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ) )
18 15 17 mpbird ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐹 = ( 𝐹 ↾ 𝐴 ) ) → 𝐹 : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )
19 8 18 mpdan ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )