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