This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f2ndf

Description: The 2nd (second component of an ordered pair) function restricted to a function F is a function from F into the codomain of F . (Contributed by Alexander van der Vekens, 4-Feb-2018)

		Ref	Expression
	Assertion	f2ndf	$⊢ F : A ⟶ B \to ({2^{nd} ↾}_{F}) : F ⟶ B$

Proof

Step	Hyp	Ref	Expression
1		f2ndres	$⊢ ({2^{nd} ↾}_{(A \times B)}) : A \times B ⟶ B$
2		fssxp	$⊢ F : A ⟶ B \to F \subseteq A \times B$
3		fssres	$⊢ (({2^{nd} ↾}_{(A \times B)}) : A \times B ⟶ B \land F \subseteq A \times B) \to ({({2^{nd} ↾}_{(A \times B)}) ↾}_{F}) : F ⟶ B$
4	1 2 3	sylancr	$⊢ F : A ⟶ B \to ({({2^{nd} ↾}_{(A \times B)}) ↾}_{F}) : F ⟶ B$
5	2	resabs1d	$⊢ F : A ⟶ B \to {({2^{nd} ↾}_{(A \times B)}) ↾}_{F} = {2^{nd} ↾}_{F}$
6	5	eqcomd	$⊢ F : A ⟶ B \to {2^{nd} ↾}_{F} = {({2^{nd} ↾}_{(A \times B)}) ↾}_{F}$
7	6	feq1d	$⊢ F : A ⟶ B \to (({2^{nd} ↾}_{F}) : F ⟶ B \leftrightarrow ({({2^{nd} ↾}_{(A \times B)}) ↾}_{F}) : F ⟶ B)$
8	4 7	mpbird	$⊢ F : A ⟶ B \to ({2^{nd} ↾}_{F}) : F ⟶ B$