Theorem df2nd2

Description: An alternate possible definition of the 2nd function. (Contributed by NM, 10-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	df2nd2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } = ( 2nd ↾ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		fo2nd	⊢ 2nd : V –onto→ V
2		fofn	⊢ ( 2nd : V –onto→ V → 2nd Fn V )
3	1 2	ax-mp	⊢ 2nd Fn V
4		dffn5	⊢ ( 2nd Fn V ↔ 2nd = ( 𝑤 ∈ V ↦ ( 2nd ‘ 𝑤 ) ) )
5	3 4	mpbi	⊢ 2nd = ( 𝑤 ∈ V ↦ ( 2nd ‘ 𝑤 ) )
6		mptv	⊢ ( 𝑤 ∈ V ↦ ( 2nd ‘ 𝑤 ) ) = { ⟨ 𝑤 , 𝑧 ⟩ ∣ 𝑧 = ( 2nd ‘ 𝑤 ) }
7	5 6	eqtri	⊢ 2nd = { ⟨ 𝑤 , 𝑧 ⟩ ∣ 𝑧 = ( 2nd ‘ 𝑤 ) }
8	7	reseq1i	⊢ ( 2nd ↾ ( V × V ) ) = ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ 𝑧 = ( 2nd ‘ 𝑤 ) } ↾ ( V × V ) )
9		resopab	⊢ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ 𝑧 = ( 2nd ‘ 𝑤 ) } ↾ ( V × V ) ) = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ 𝑧 = ( 2nd ‘ 𝑤 ) ) }
10		vex	⊢ 𝑥 ∈ V
11		vex	⊢ 𝑦 ∈ V
12	10 11	op2ndd	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑤 ) = 𝑦 )
13	12	eqeq2d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 = ( 2nd ‘ 𝑤 ) ↔ 𝑧 = 𝑦 ) )
14	13	dfoprab3	⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ ( V × V ) ∧ 𝑧 = ( 2nd ‘ 𝑤 ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 }
15	8 9 14	3eqtrri	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } = ( 2nd ↾ ( V × V ) )