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

Metamath Proof Explorer

Theorem otel3xp

Description: An ordered triple is an element of a doubled Cartesian product. (Contributed by Alexander van der Vekens, 26-Feb-2018)

Ref Expression
Assertion otel3xp ( ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ) → 𝑇 ∈ ( ( 𝑋 × 𝑌 ) × 𝑍 ) )

Proof

Step Hyp Ref Expression
1 df-ot ⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩
2 3simpa ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) )
3 opelxp ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) )
4 2 3 sylibr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) )
5 simp3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝐶 ∈ 𝑍 )
6 4 5 opelxpd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ ( ( 𝑋 × 𝑌 ) × 𝑍 ) )
7 1 6 eqeltrid ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∈ ( ( 𝑋 × 𝑌 ) × 𝑍 ) )
8 eleq1 ⊢ ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( 𝑇 ∈ ( ( 𝑋 × 𝑌 ) × 𝑍 ) ↔ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∈ ( ( 𝑋 × 𝑌 ) × 𝑍 ) ) )
9 7 8 imbitrrid ⊢ ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝑇 ∈ ( ( 𝑋 × 𝑌 ) × 𝑍 ) ) )
10 9 imp ⊢ ( ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ) → 𝑇 ∈ ( ( 𝑋 × 𝑌 ) × 𝑍 ) )