oteqimp

Description: The components of an ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018)

		Ref	Expression
	Assertion	oteqimp	$⊢ T = ⟨A, B, C⟩ \to ((A \in X \land B \in Y \land C \in Z) \to (1^{st} (1^{st} (T)) = A \land 2^{nd} (1^{st} (T)) = B \land 2^{nd} (T) = C))$

Step	Hyp	Ref	Expression
1		ot1stg	$⊢ (A \in X \land B \in Y \land C \in Z) \to 1^{st} (1^{st} (⟨A, B, C⟩)) = A$
2		ot2ndg	$⊢ (A \in X \land B \in Y \land C \in Z) \to 2^{nd} (1^{st} (⟨A, B, C⟩)) = B$
3		ot3rdg	$⊢ C \in Z \to 2^{nd} (⟨A, B, C⟩) = C$
4	3	3ad2ant3	$⊢ (A \in X \land B \in Y \land C \in Z) \to 2^{nd} (⟨A, B, C⟩) = C$
5	1 2 4	3jca	$⊢ (A \in X \land B \in Y \land C \in Z) \to (1^{st} (1^{st} (⟨A, B, C⟩)) = A \land 2^{nd} (1^{st} (⟨A, B, C⟩)) = B \land 2^{nd} (⟨A, B, C⟩) = C)$
6		2fveq3	$⊢ T = ⟨A, B, C⟩ \to 1^{st} (1^{st} (T)) = 1^{st} (1^{st} (⟨A, B, C⟩))$
7	6	eqeq1d	$⊢ T = ⟨A, B, C⟩ \to (1^{st} (1^{st} (T)) = A \leftrightarrow 1^{st} (1^{st} (⟨A, B, C⟩)) = A)$
8		2fveq3	$⊢ T = ⟨A, B, C⟩ \to 2^{nd} (1^{st} (T)) = 2^{nd} (1^{st} (⟨A, B, C⟩))$
9	8	eqeq1d	$⊢ T = ⟨A, B, C⟩ \to (2^{nd} (1^{st} (T)) = B \leftrightarrow 2^{nd} (1^{st} (⟨A, B, C⟩)) = B)$
10		fveqeq2	$⊢ T = ⟨A, B, C⟩ \to (2^{nd} (T) = C \leftrightarrow 2^{nd} (⟨A, B, C⟩) = C)$
11	7 9 10	3anbi123d	$⊢ T = ⟨A, B, C⟩ \to ((1^{st} (1^{st} (T)) = A \land 2^{nd} (1^{st} (T)) = B \land 2^{nd} (T) = C) \leftrightarrow (1^{st} (1^{st} (⟨A, B, C⟩)) = A \land 2^{nd} (1^{st} (⟨A, B, C⟩)) = B \land 2^{nd} (⟨A, B, C⟩) = C))$
12	5 11	imbitrrid	$⊢ T = ⟨A, B, C⟩ \to ((A \in X \land B \in Y \land C \in Z) \to (1^{st} (1^{st} (T)) = A \land 2^{nd} (1^{st} (T)) = B \land 2^{nd} (T) = C))$

Metamath Proof Explorer