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	syl5ibr	⊢ ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) → 𝑇 ∈ ( ( 𝑋 × 𝑌 ) × 𝑍 ) ) )
10	9	imp	⊢ ( ( 𝑇 = ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍 ) ) → 𝑇 ∈ ( ( 𝑋 × 𝑌 ) × 𝑍 ) )