This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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