fores

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

		Ref	Expression
	Assertion	fores	$⊢ (Fun F \land A \subseteq dom F) \to ({F ↾}_{A}) : A \underset{onto}{⟶} F [A]$

Step	Hyp	Ref	Expression
1		funres	$⊢ Fun F \to Fun ({F ↾}_{A})$
2	1	anim1i	$⊢ (Fun F \land A \subseteq dom F) \to (Fun ({F ↾}_{A}) \land A \subseteq dom F)$
3		df-fn	$⊢ ({F ↾}_{A}) Fn A \leftrightarrow (Fun ({F ↾}_{A}) \land dom ({F ↾}_{A}) = A)$
4		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
5	4	eqcomi	$⊢ ran ({F ↾}_{A}) = F [A]$
6		df-fo	$⊢ ({F ↾}_{A}) : A \underset{onto}{⟶} F [A] \leftrightarrow (({F ↾}_{A}) Fn A \land ran ({F ↾}_{A}) = F [A])$
7	5 6	mpbiran2	$⊢ ({F ↾}_{A}) : A \underset{onto}{⟶} F [A] \leftrightarrow ({F ↾}_{A}) Fn A$
8		ssdmres	$⊢ A \subseteq dom F \leftrightarrow dom ({F ↾}_{A}) = A$
9	8	anbi2i	$⊢ (Fun ({F ↾}_{A}) \land A \subseteq dom F) \leftrightarrow (Fun ({F ↾}_{A}) \land dom ({F ↾}_{A}) = A)$
10	3 7 9	3bitr4i	$⊢ ({F ↾}_{A}) : A \underset{onto}{⟶} F [A] \leftrightarrow (Fun ({F ↾}_{A}) \land A \subseteq dom F)$
11	2 10	sylibr	$⊢ (Fun F \land A \subseteq dom F) \to ({F ↾}_{A}) : A \underset{onto}{⟶} F [A]$

Metamath Proof Explorer