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	biimpi	⊢ ( Fun 𝐹 → 𝐹 Fn dom 𝐹 )
3	2	adantr	⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ) → 𝐹 Fn dom 𝐹 )
4		sseqin2	⊢ ( 𝐶 ⊆ ran 𝐹 ↔ ( ran 𝐹 ∩ 𝐶 ) = 𝐶 )
5	4	biimpi	⊢ ( 𝐶 ⊆ ran 𝐹 → ( ran 𝐹 ∩ 𝐶 ) = 𝐶 )
6	5	eqcomd	⊢ ( 𝐶 ⊆ ran 𝐹 → 𝐶 = ( ran 𝐹 ∩ 𝐶 ) )
7	6	adantl	⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ) → 𝐶 = ( ran 𝐹 ∩ 𝐶 ) )
8		eqidd	⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ) → ( ◡ 𝐹 “ 𝐶 ) = ( ◡ 𝐹 “ 𝐶 ) )
9	3 7 8	rescnvimafod	⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ) → ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) : ( ◡ 𝐹 “ 𝐶 ) –onto→ 𝐶 )