Metamath Proof Explorer


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 ) )