el2xptp0

Description: A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018)

		Ref	Expression
	Assertion	el2xptp0	$⊢ (X \in U \land Y \in V \land Z \in W) \to ((A \in ((U \times V) \times W) \land (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z)) \leftrightarrow A = ⟨X, Y, Z⟩)$

Proof

Step	Hyp	Ref	Expression
1		xp1st	$⊢ A \in ((U \times V) \times W) \to 1^{st} (A) \in (U \times V)$
2	1	ad2antrl	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in ((U \times V) \times W) \land (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z))) \to 1^{st} (A) \in (U \times V)$
3		3simpa	$⊢ (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z) \to (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y)$
4	3	adantl	$⊢ (A \in ((U \times V) \times W) \land (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z)) \to (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y)$
5	4	adantl	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in ((U \times V) \times W) \land (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z))) \to (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y)$
6		eqopi	$⊢ (1^{st} (A) \in (U \times V) \land (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y)) \to 1^{st} (A) = ⟨X, Y⟩$
7	2 5 6	syl2anc	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in ((U \times V) \times W) \land (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z))) \to 1^{st} (A) = ⟨X, Y⟩$
8		simprr3	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in ((U \times V) \times W) \land (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z))) \to 2^{nd} (A) = Z$
9	7 8	jca	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in ((U \times V) \times W) \land (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z))) \to (1^{st} (A) = ⟨X, Y⟩ \land 2^{nd} (A) = Z)$
10		df-ot	$⊢ ⟨X, Y, Z⟩ = ⟨⟨X, Y⟩, Z⟩$
11	10	eqeq2i	$⊢ A = ⟨X, Y, Z⟩ \leftrightarrow A = ⟨⟨X, Y⟩, Z⟩$
12		eqop	$⊢ A \in ((U \times V) \times W) \to (A = ⟨⟨X, Y⟩, Z⟩ \leftrightarrow (1^{st} (A) = ⟨X, Y⟩ \land 2^{nd} (A) = Z))$
13	11 12	bitrid	$⊢ A \in ((U \times V) \times W) \to (A = ⟨X, Y, Z⟩ \leftrightarrow (1^{st} (A) = ⟨X, Y⟩ \land 2^{nd} (A) = Z))$
14	13	ad2antrl	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in ((U \times V) \times W) \land (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z))) \to (A = ⟨X, Y, Z⟩ \leftrightarrow (1^{st} (A) = ⟨X, Y⟩ \land 2^{nd} (A) = Z))$
15	9 14	mpbird	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in ((U \times V) \times W) \land (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z))) \to A = ⟨X, Y, Z⟩$
16		opelxpi	$⊢ (X \in U \land Y \in V) \to ⟨X, Y⟩ \in (U \times V)$
17	16	3adant3	$⊢ (X \in U \land Y \in V \land Z \in W) \to ⟨X, Y⟩ \in (U \times V)$
18		simp3	$⊢ (X \in U \land Y \in V \land Z \in W) \to Z \in W$
19	17 18	opelxpd	$⊢ (X \in U \land Y \in V \land Z \in W) \to ⟨⟨X, Y⟩, Z⟩ \in ((U \times V) \times W)$
20	10 19	eqeltrid	$⊢ (X \in U \land Y \in V \land Z \in W) \to ⟨X, Y, Z⟩ \in ((U \times V) \times W)$
21	20	adantr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land A = ⟨X, Y, Z⟩) \to ⟨X, Y, Z⟩ \in ((U \times V) \times W)$
22		eleq1	$⊢ A = ⟨X, Y, Z⟩ \to (A \in ((U \times V) \times W) \leftrightarrow ⟨X, Y, Z⟩ \in ((U \times V) \times W))$
23	22	adantl	$⊢ ((X \in U \land Y \in V \land Z \in W) \land A = ⟨X, Y, Z⟩) \to (A \in ((U \times V) \times W) \leftrightarrow ⟨X, Y, Z⟩ \in ((U \times V) \times W))$
24	21 23	mpbird	$⊢ ((X \in U \land Y \in V \land Z \in W) \land A = ⟨X, Y, Z⟩) \to A \in ((U \times V) \times W)$
25		2fveq3	$⊢ A = ⟨X, Y, Z⟩ \to 1^{st} (1^{st} (A)) = 1^{st} (1^{st} (⟨X, Y, Z⟩))$
26		ot1stg	$⊢ (X \in U \land Y \in V \land Z \in W) \to 1^{st} (1^{st} (⟨X, Y, Z⟩)) = X$
27	25 26	sylan9eqr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land A = ⟨X, Y, Z⟩) \to 1^{st} (1^{st} (A)) = X$
28		2fveq3	$⊢ A = ⟨X, Y, Z⟩ \to 2^{nd} (1^{st} (A)) = 2^{nd} (1^{st} (⟨X, Y, Z⟩))$
29		ot2ndg	$⊢ (X \in U \land Y \in V \land Z \in W) \to 2^{nd} (1^{st} (⟨X, Y, Z⟩)) = Y$
30	28 29	sylan9eqr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land A = ⟨X, Y, Z⟩) \to 2^{nd} (1^{st} (A)) = Y$
31		fveq2	$⊢ A = ⟨X, Y, Z⟩ \to 2^{nd} (A) = 2^{nd} (⟨X, Y, Z⟩)$
32		ot3rdg	$⊢ Z \in W \to 2^{nd} (⟨X, Y, Z⟩) = Z$
33	32	3ad2ant3	$⊢ (X \in U \land Y \in V \land Z \in W) \to 2^{nd} (⟨X, Y, Z⟩) = Z$
34	31 33	sylan9eqr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land A = ⟨X, Y, Z⟩) \to 2^{nd} (A) = Z$
35	27 30 34	3jca	$⊢ ((X \in U \land Y \in V \land Z \in W) \land A = ⟨X, Y, Z⟩) \to (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z)$
36	24 35	jca	$⊢ ((X \in U \land Y \in V \land Z \in W) \land A = ⟨X, Y, Z⟩) \to (A \in ((U \times V) \times W) \land (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z))$
37	15 36	impbida	$⊢ (X \in U \land Y \in V \land Z \in W) \to ((A \in ((U \times V) \times W) \land (1^{st} (1^{st} (A)) = X \land 2^{nd} (1^{st} (A)) = Y \land 2^{nd} (A) = Z)) \leftrightarrow A = ⟨X, Y, Z⟩)$

Metamath Proof Explorer

Theorem el2xptp0

Proof