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

Metamath Proof Explorer

Theorem xp2nd

Description: Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion xp2nd ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ( 2nd ‘ 𝐴 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 elxp ⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑏 ∃ 𝑐 ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) )
2 vex ⊢ 𝑏 ∈ V
3 vex ⊢ 𝑐 ∈ V
4 2 3 op2ndd ⊢ ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ → ( 2nd ‘ 𝐴 ) = 𝑐 )
5 4 eleq1d ⊢ ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ → ( ( 2nd ‘ 𝐴 ) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶 ) )
6 5 biimpar ⊢ ( ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑐 ∈ 𝐶 ) → ( 2nd ‘ 𝐴 ) ∈ 𝐶 )
7 6 adantrl ⊢ ( ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 2nd ‘ 𝐴 ) ∈ 𝐶 )
8 7 exlimivv ⊢ ( ∃ 𝑏 ∃ 𝑐 ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 2nd ‘ 𝐴 ) ∈ 𝐶 )
9 1 8 sylbi ⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ( 2nd ‘ 𝐴 ) ∈ 𝐶 )