Theorem fresfo

Description: Conditions for a restriction to be an onto function. Part of fresf1o . (Contributed by AV, 29-Sep-2024)

	Ref	Expression
Assertion	fresfo	⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ) → ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) : ( ◡ 𝐹 “ 𝐶 ) –onto→ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
2	1	birani	⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ) → 𝐹 Fn dom 𝐹 )
3		sseqin2	⊢ ( 𝐶 ⊆ ran 𝐹 ↔ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 )
4	3	biimpi	⊢ ( 𝐶 ⊆ ran 𝐹 → ( ran 𝐹 ∩ 𝐶 ) = 𝐶 )
5	4	eqcomd	⊢ ( 𝐶 ⊆ ran 𝐹 → 𝐶 = ( ran 𝐹 ∩ 𝐶 ) )
6	5	adantl	⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ) → 𝐶 = ( ran 𝐹 ∩ 𝐶 ) )
7		eqidd	⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ) → ( ◡ 𝐹 “ 𝐶 ) = ( ◡ 𝐹 “ 𝐶 ) )
8	2 6 7	rescnvimafod	⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ) → ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) : ( ◡ 𝐹 “ 𝐶 ) –onto→ 𝐶 )