fo2ndres

Description: Onto mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 14-Dec-2008)

		Ref	Expression
	Assertion	fo2ndres	$⊢ A \neq \emptyset \to ({2^{nd} ↾}_{(A \times B)}) : A \times B \underset{onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
2		opelxp	$⊢ ⟨x, y⟩ \in (A \times B) \leftrightarrow (x \in A \land y \in B)$
3		fvres	$⊢ ⟨x, y⟩ \in (A \times B) \to ({2^{nd} ↾}_{(A \times B)}) (⟨x, y⟩) = 2^{nd} (⟨x, y⟩)$
4		vex	$⊢ x \in V$
5		vex	$⊢ y \in V$
6	4 5	op2nd	$⊢ 2^{nd} (⟨x, y⟩) = y$
7	3 6	eqtr2di	$⊢ ⟨x, y⟩ \in (A \times B) \to y = ({2^{nd} ↾}_{(A \times B)}) (⟨x, y⟩)$
8		f2ndres	$⊢ ({2^{nd} ↾}_{(A \times B)}) : A \times B ⟶ B$
9		ffn	$⊢ ({2^{nd} ↾}_{(A \times B)}) : A \times B ⟶ B \to ({2^{nd} ↾}_{(A \times B)}) Fn (A \times B)$
10	8 9	ax-mp	$⊢ ({2^{nd} ↾}_{(A \times B)}) Fn (A \times B)$
11		fnfvelrn	$⊢ (({2^{nd} ↾}_{(A \times B)}) Fn (A \times B) \land ⟨x, y⟩ \in (A \times B)) \to ({2^{nd} ↾}_{(A \times B)}) (⟨x, y⟩) \in ran ({2^{nd} ↾}_{(A \times B)})$
12	10 11	mpan	$⊢ ⟨x, y⟩ \in (A \times B) \to ({2^{nd} ↾}_{(A \times B)}) (⟨x, y⟩) \in ran ({2^{nd} ↾}_{(A \times B)})$
13	7 12	eqeltrd	$⊢ ⟨x, y⟩ \in (A \times B) \to y \in ran ({2^{nd} ↾}_{(A \times B)})$
14	2 13	sylbir	$⊢ (x \in A \land y \in B) \to y \in ran ({2^{nd} ↾}_{(A \times B)})$
15	14	ex	$⊢ x \in A \to (y \in B \to y \in ran ({2^{nd} ↾}_{(A \times B)}))$
16	15	exlimiv	$⊢ \exists x x \in A \to (y \in B \to y \in ran ({2^{nd} ↾}_{(A \times B)}))$
17	1 16	sylbi	$⊢ A \neq \emptyset \to (y \in B \to y \in ran ({2^{nd} ↾}_{(A \times B)}))$
18	17	ssrdv	$⊢ A \neq \emptyset \to B \subseteq ran ({2^{nd} ↾}_{(A \times B)})$
19		frn	$⊢ ({2^{nd} ↾}_{(A \times B)}) : A \times B ⟶ B \to ran ({2^{nd} ↾}_{(A \times B)}) \subseteq B$
20	8 19	ax-mp	$⊢ ran ({2^{nd} ↾}_{(A \times B)}) \subseteq B$
21	18 20	jctil	$⊢ A \neq \emptyset \to (ran ({2^{nd} ↾}_{(A \times B)}) \subseteq B \land B \subseteq ran ({2^{nd} ↾}_{(A \times B)}))$
22		eqss	$⊢ ran ({2^{nd} ↾}_{(A \times B)}) = B \leftrightarrow (ran ({2^{nd} ↾}_{(A \times B)}) \subseteq B \land B \subseteq ran ({2^{nd} ↾}_{(A \times B)}))$
23	21 22	sylibr	$⊢ A \neq \emptyset \to ran ({2^{nd} ↾}_{(A \times B)}) = B$
24	23 8	jctil	$⊢ A \neq \emptyset \to (({2^{nd} ↾}_{(A \times B)}) : A \times B ⟶ B \land ran ({2^{nd} ↾}_{(A \times B)}) = B)$
25		dffo2	$⊢ ({2^{nd} ↾}_{(A \times B)}) : A \times B \underset{onto}{⟶} B \leftrightarrow (({2^{nd} ↾}_{(A \times B)}) : A \times B ⟶ B \land ran ({2^{nd} ↾}_{(A \times B)}) = B)$
26	24 25	sylibr	$⊢ A \neq \emptyset \to ({2^{nd} ↾}_{(A \times B)}) : A \times B \underset{onto}{⟶} B$

Metamath Proof Explorer

Theorem fo2ndres

Proof