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	bilanri	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 )
6	5	rgen2	⊢ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵
7		sneq	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → { 𝑥 } = { ⟨ 𝑦 , 𝑧 ⟩ } )
8	7	rneqd	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ran { 𝑥 } = ran { ⟨ 𝑦 , 𝑧 ⟩ } )
9	8	unieqd	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ∪ ran { 𝑥 } = ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } )
10	9	eleq1d	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ∪ ran { 𝑥 } ∈ 𝐵 ↔ ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 ) )
11	10	ralxp	⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ ran { 𝑥 } ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ∪ ran { ⟨ 𝑦 , 𝑧 ⟩ } ∈ 𝐵 )
12	6 11	mpbir	⊢ ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ ran { 𝑥 } ∈ 𝐵
13		df-2nd	⊢ 2nd = ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } )
14	13	reseq1i	⊢ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) )
15		ssv	⊢ ( 𝐴 × 𝐵 ) ⊆ V
16		resmpt	⊢ ( ( 𝐴 × 𝐵 ) ⊆ V → ( ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ran { 𝑥 } ) )
17	15 16	ax-mp	⊢ ( ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } ) ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ran { 𝑥 } )
18	14 17	eqtri	⊢ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ran { 𝑥 } )
19	18	fmpt	⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐵 ) ∪ ran { 𝑥 } ∈ 𝐵 ↔ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵 )
20	12 19	mpbi	⊢ ( 2nd ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐵