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	$⊢ (T = ⟨A, B, C⟩ \land (A \in X \land B \in Y \land C \in Z)) \to T \in ((X \times Y) \times Z)$

Step	Hyp	Ref	Expression
1		df-ot	$⊢ ⟨A, B, C⟩ = ⟨⟨A, B⟩, C⟩$
2		3simpa	$⊢ (A \in X \land B \in Y \land C \in Z) \to (A \in X \land B \in Y)$
3		opelxp	$⊢ ⟨A, B⟩ \in (X \times Y) \leftrightarrow (A \in X \land B \in Y)$
4	2 3	sylibr	$⊢ (A \in X \land B \in Y \land C \in Z) \to ⟨A, B⟩ \in (X \times Y)$
5		simp3	$⊢ (A \in X \land B \in Y \land C \in Z) \to C \in Z$
6	4 5	opelxpd	$⊢ (A \in X \land B \in Y \land C \in Z) \to ⟨⟨A, B⟩, C⟩ \in ((X \times Y) \times Z)$
7	1 6	eqeltrid	$⊢ (A \in X \land B \in Y \land C \in Z) \to ⟨A, B, C⟩ \in ((X \times Y) \times Z)$
8		eleq1	$⊢ T = ⟨A, B, C⟩ \to (T \in ((X \times Y) \times Z) \leftrightarrow ⟨A, B, C⟩ \in ((X \times Y) \times Z))$
9	7 8	syl5ibr	$⊢ T = ⟨A, B, C⟩ \to ((A \in X \land B \in Y \land C \in Z) \to T \in ((X \times Y) \times Z))$
10	9	imp	$⊢ (T = ⟨A, B, C⟩ \land (A \in X \land B \in Y \land C \in Z)) \to T \in ((X \times Y) \times Z)$

Metamath Proof Explorer