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 F \land C \subseteq ran F) \to ({F ↾}_{F^{-1} [C]}) : F^{-1} [C] \underset{onto}{⟶} C$

Step	Hyp	Ref	Expression
1		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
2	1	birani	$⊢ (Fun F \land C \subseteq ran F) \to F Fn dom F$
3		sseqin2	$⊢ C \subseteq ran F \leftrightarrow ran F \cap C = C$
4	3	biimpi	$⊢ C \subseteq ran F \to ran F \cap C = C$
5	4	eqcomd	$⊢ C \subseteq ran F \to C = ran F \cap C$
6	5	adantl	$⊢ (Fun F \land C \subseteq ran F) \to C = ran F \cap C$
7		eqidd	$⊢ (Fun F \land C \subseteq ran F) \to F^{-1} [C] = F^{-1} [C]$
8	2 6 7	rescnvimafod	$⊢ (Fun F \land C \subseteq ran F) \to ({F ↾}_{F^{-1} [C]}) : F^{-1} [C] \underset{onto}{⟶} C$

Metamath Proof Explorer