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

Metamath Proof Explorer

Theorem 2ndval2

Description: Alternate value of the function that extracts the second member of an ordered pair. Definition 5.13 (ii) of Monk1 p. 52. (Contributed by NM, 18-Aug-2006)

Ref Expression
Assertion 2ndval2 ( 𝐴 ∈ ( V × V ) → ( 2nd ‘ 𝐴 ) = ∩ ∩ ∩ ◡ { 𝐴 } )

Proof

Step Hyp Ref Expression
1 elvv ⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
2 vex ⊢ 𝑥 ∈ V
3 vex ⊢ 𝑦 ∈ V
4 2 3 op2nd ⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
5 2 3 op2ndb ⊢ ∩ ∩ ∩ ◡ { ⟨ 𝑥 , 𝑦 ⟩ } = 𝑦
6 4 5 eqtr4i ⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ∩ ∩ ∩ ◡ { ⟨ 𝑥 , 𝑦 ⟩ }
7 fveq2 ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝐴 ) = ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
8 sneq ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → { 𝐴 } = { ⟨ 𝑥 , 𝑦 ⟩ } )
9 8 cnveqd ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ◡ { 𝐴 } = ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
10 9 inteqd ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∩ ◡ { 𝐴 } = ∩ ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
11 10 inteqd ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∩ ∩ ◡ { 𝐴 } = ∩ ∩ ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
12 11 inteqd ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∩ ∩ ∩ ◡ { 𝐴 } = ∩ ∩ ∩ ◡ { ⟨ 𝑥 , 𝑦 ⟩ } )
13 6 7 12 3eqtr4a ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝐴 ) = ∩ ∩ ∩ ◡ { 𝐴 } )
14 13 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝐴 ) = ∩ ∩ ∩ ◡ { 𝐴 } )
15 1 14 sylbi ⊢ ( 𝐴 ∈ ( V × V ) → ( 2nd ‘ 𝐴 ) = ∩ ∩ ∩ ◡ { 𝐴 } )