f2ndres

Description: Mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 7-Aug-2006) (Revised by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Assertion	f2ndres	$⊢ ({2^{nd} ↾}_{(A \times B)}) : A \times B ⟶ B$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ y \in V$
2		vex	$⊢ z \in V$
3	1 2	op2nda	$⊢ ⋃ ran \{⟨y, z⟩\} = z$
4	3	eleq1i	$⊢ ⋃ ran \{⟨y, z⟩\} \in B \leftrightarrow z \in B$
5	4	bilanri	$⊢ (y \in A \land z \in B) \to ⋃ ran \{⟨y, z⟩\} \in B$
6	5	rgen2	$⊢ \forall y \in A \forall z \in B ⋃ ran \{⟨y, z⟩\} \in B$
7		sneq	$⊢ x = ⟨y, z⟩ \to \{x\} = \{⟨y, z⟩\}$
8	7	rneqd	$⊢ x = ⟨y, z⟩ \to ran \{x\} = ran \{⟨y, z⟩\}$
9	8	unieqd	$⊢ x = ⟨y, z⟩ \to ⋃ ran \{x\} = ⋃ ran \{⟨y, z⟩\}$
10	9	eleq1d	$⊢ x = ⟨y, z⟩ \to (⋃ ran \{x\} \in B \leftrightarrow ⋃ ran \{⟨y, z⟩\} \in B)$
11	10	ralxp	$⊢ \forall x \in (A \times B) ⋃ ran \{x\} \in B \leftrightarrow \forall y \in A \forall z \in B ⋃ ran \{⟨y, z⟩\} \in B$
12	6 11	mpbir	$⊢ \forall x \in (A \times B) ⋃ ran \{x\} \in B$
13		df-2nd	$⊢ 2^{nd} = (x \in V ⟼ ⋃ ran \{x\})$
14	13	reseq1i	$⊢ {2^{nd} ↾}_{(A \times B)} = {(x \in V ⟼ ⋃ ran \{x\}) ↾}_{(A \times B)}$
15		ssv	$⊢ A \times B \subseteq V$
16		resmpt	$⊢ A \times B \subseteq V \to {(x \in V ⟼ ⋃ ran \{x\}) ↾}_{(A \times B)} = (x \in (A \times B) ⟼ ⋃ ran \{x\})$
17	15 16	ax-mp	$⊢ {(x \in V ⟼ ⋃ ran \{x\}) ↾}_{(A \times B)} = (x \in (A \times B) ⟼ ⋃ ran \{x\})$
18	14 17	eqtri	$⊢ {2^{nd} ↾}_{(A \times B)} = (x \in (A \times B) ⟼ ⋃ ran \{x\})$
19	18	fmpt	$⊢ \forall x \in (A \times B) ⋃ ran \{x\} \in B \leftrightarrow ({2^{nd} ↾}_{(A \times B)}) : A \times B ⟶ B$
20	12 19	mpbi	$⊢ ({2^{nd} ↾}_{(A \times B)}) : A \times B ⟶ B$

Metamath Proof Explorer

Theorem f2ndres

Proof