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	biimpi	$⊢ Fun F \to F Fn dom F$
3	2	adantr	$⊢ (Fun F \land C \subseteq ran F) \to F Fn dom F$
4		sseqin2	$⊢ C \subseteq ran F \leftrightarrow ran F \cap C = C$
5	4	biimpi	$⊢ C \subseteq ran F \to ran F \cap C = C$
6	5	eqcomd	$⊢ C \subseteq ran F \to C = ran F \cap C$
7	6	adantl	$⊢ (Fun F \land C \subseteq ran F) \to C = ran F \cap C$
8		eqidd	$⊢ (Fun F \land C \subseteq ran F) \to F^{-1} [C] = F^{-1} [C]$
9	3 7 8	rescnvimafod	$⊢ (Fun F \land C \subseteq ran F) \to ({F ↾}_{F^{-1} [C]}) : F^{-1} [C] \underset{onto}{⟶} C$

Metamath Proof Explorer