fo2ndf

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

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

Proof

Step	Hyp	Ref	Expression
1		ffrn	$⊢ F : A ⟶ B \to F : A ⟶ ran F$
2		f2ndf	$⊢ F : A ⟶ ran F \to ({2^{nd} ↾}_{F}) : F ⟶ ran F$
3	1 2	syl	$⊢ F : A ⟶ B \to ({2^{nd} ↾}_{F}) : F ⟶ ran F$
4		ffn	$⊢ F : A ⟶ B \to F Fn A$
5		dffn3	$⊢ F Fn A \leftrightarrow F : A ⟶ ran F$
6	5 2	sylbi	$⊢ F Fn A \to ({2^{nd} ↾}_{F}) : F ⟶ ran F$
7	4 6	syl	$⊢ F : A ⟶ B \to ({2^{nd} ↾}_{F}) : F ⟶ ran F$
8	7	frnd	$⊢ F : A ⟶ B \to ran ({2^{nd} ↾}_{F}) \subseteq ran F$
9		elrn2g	$⊢ y \in ran F \to (y \in ran F \leftrightarrow \exists x ⟨x, y⟩ \in F)$
10	9	ibi	$⊢ y \in ran F \to \exists x ⟨x, y⟩ \in F$
11		fvres	$⊢ ⟨x, y⟩ \in F \to ({2^{nd} ↾}_{F}) (⟨x, y⟩) = 2^{nd} (⟨x, y⟩)$
12	11	adantl	$⊢ (F : A ⟶ B \land ⟨x, y⟩ \in F) \to ({2^{nd} ↾}_{F}) (⟨x, y⟩) = 2^{nd} (⟨x, y⟩)$
13		vex	$⊢ x \in V$
14		vex	$⊢ y \in V$
15	13 14	op2nd	$⊢ 2^{nd} (⟨x, y⟩) = y$
16	12 15	eqtr2di	$⊢ (F : A ⟶ B \land ⟨x, y⟩ \in F) \to y = ({2^{nd} ↾}_{F}) (⟨x, y⟩)$
17		f2ndf	$⊢ F : A ⟶ B \to ({2^{nd} ↾}_{F}) : F ⟶ B$
18	17	ffnd	$⊢ F : A ⟶ B \to ({2^{nd} ↾}_{F}) Fn F$
19		fnfvelrn	$⊢ (({2^{nd} ↾}_{F}) Fn F \land ⟨x, y⟩ \in F) \to ({2^{nd} ↾}_{F}) (⟨x, y⟩) \in ran ({2^{nd} ↾}_{F})$
20	18 19	sylan	$⊢ (F : A ⟶ B \land ⟨x, y⟩ \in F) \to ({2^{nd} ↾}_{F}) (⟨x, y⟩) \in ran ({2^{nd} ↾}_{F})$
21	16 20	eqeltrd	$⊢ (F : A ⟶ B \land ⟨x, y⟩ \in F) \to y \in ran ({2^{nd} ↾}_{F})$
22	21	ex	$⊢ F : A ⟶ B \to (⟨x, y⟩ \in F \to y \in ran ({2^{nd} ↾}_{F}))$
23	22	exlimdv	$⊢ F : A ⟶ B \to (\exists x ⟨x, y⟩ \in F \to y \in ran ({2^{nd} ↾}_{F}))$
24	10 23	syl5	$⊢ F : A ⟶ B \to (y \in ran F \to y \in ran ({2^{nd} ↾}_{F}))$
25	24	ssrdv	$⊢ F : A ⟶ B \to ran F \subseteq ran ({2^{nd} ↾}_{F})$
26	8 25	eqssd	$⊢ F : A ⟶ B \to ran ({2^{nd} ↾}_{F}) = ran F$
27		dffo2	$⊢ ({2^{nd} ↾}_{F}) : F \underset{onto}{⟶} ran F \leftrightarrow (({2^{nd} ↾}_{F}) : F ⟶ ran F \land ran ({2^{nd} ↾}_{F}) = ran F)$
28	3 26 27	sylanbrc	$⊢ F : A ⟶ B \to ({2^{nd} ↾}_{F}) : F \underset{onto}{⟶} ran F$

Metamath Proof Explorer

Theorem fo2ndf

Proof