Theorem 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	⊢ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑦 ∈ V
2		vex	⊢ 𝑧 ∈ V
3	1 2	op2nda	⊢ ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } = 𝑧
4	3	eleq1i	⊢ ( ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 )
5	4	biimpri	⊢ ( 𝑧 ∈ 𝐵 → ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 )
6	5	adantl	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 )
7	6	rgen2	⊢ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵
8		sneq	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → { 𝑥 } = { ⟨ 𝑦 , 𝑧 ⟩ } )
9	8	rneqd	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ran { 𝑥 } = ran { ⟨ 𝑦 , 𝑧 ⟩ } )
10	9	unieqd	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ∪ ran { 𝑥 } = ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } )
11	10	eleq1d	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ∪ ran { 𝑥 } ∈ 𝐵 ↔ ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 ) )
12	11	ralxp	⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ ran { 𝑥 } ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 )
13	7 12	mpbir	⊢ ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ ran { 𝑥 } ∈ 𝐵
14		df-2nd	⊢ 2nd = ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } )
15	14	reseq1i	⊢ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) )
16		ssv	⊢ ( 𝐴 × 𝐵 ) ⊆ V
17		resmpt	⊢ ( ( 𝐴 × 𝐵 ) ⊆ V → ( ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ran { 𝑥 } ) )
18	16 17	ax-mp	⊢ ( ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ran { 𝑥 } )
19	15 18	eqtri	⊢ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ran { 𝑥 } )
20	19	fmpt	⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ ran { 𝑥 } ∈ 𝐵 ↔ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵 )
21	13 20	mpbi	⊢ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵