Theorem fores

Description: Restriction of an onto function. (Contributed by NM, 4-Mar-1997)

	Ref	Expression
Assertion	fores	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		funres	⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝐴 ) )
2	1	anim1i	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( Fun ( 𝐹 ↾ 𝐴 ) ∧ 𝐴 ⊆ dom 𝐹 ) )
3		df-fn	⊢ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ↔ ( Fun ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ) )
4		df-ima	⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
5	4	eqcomi	⊢ ran ( 𝐹 ↾ 𝐴 ) = ( 𝐹 “ 𝐴 )
6		df-fo	⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ↔ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ∧ ran ( 𝐹 ↾ 𝐴 ) = ( 𝐹 “ 𝐴 ) ) )
7	5 6	mpbiran2	⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
8		ssdmres	⊢ ( 𝐴 ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ 𝐴 ) = 𝐴 )
9	8	anbi2i	⊢ ( ( Fun ( 𝐹 ↾ 𝐴 ) ∧ 𝐴 ⊆ dom 𝐹 ) ↔ ( Fun ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ) )
10	3 7 9	3bitr4i	⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ↔ ( Fun ( 𝐹 ↾ 𝐴 ) ∧ 𝐴 ⊆ dom 𝐹 ) )
11	2 10	sylibr	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )