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	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) ↔ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		xp1st	⊢ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) → ( 1^st ‘ 𝐴 ) ∈ ( 𝑈 × 𝑉 ) )
2	1	ad2antrl	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) ) → ( 1^st ‘ 𝐴 ) ∈ ( 𝑈 × 𝑉 ) )
3		3simpa	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) → ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ) )
4	3	adantl	⊢ ( ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ) )
5	4	adantl	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ) )
6		eqopi	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ ( 𝑈 × 𝑉 ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ) ) → ( 1^st ‘ 𝐴 ) = ⟨ 𝑋 , 𝑌 ⟩ )
7	2 5 6	syl2anc	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) ) → ( 1^st ‘ 𝐴 ) = ⟨ 𝑋 , 𝑌 ⟩ )
8		simprr3	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) ) → ( 2^nd ‘ 𝐴 ) = 𝑍 )
9	7 8	jca	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) ) → ( ( 1^st ‘ 𝐴 ) = ⟨ 𝑋 , 𝑌 ⟩ ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) )
10		df-ot	⊢ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩
11	10	eqeq2i	⊢ ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ↔ 𝐴 = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ )
12		eqop	⊢ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) → ( 𝐴 = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ↔ ( ( 1^st ‘ 𝐴 ) = ⟨ 𝑋 , 𝑌 ⟩ ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) )
13	11 12	bitrid	⊢ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) → ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ↔ ( ( 1^st ‘ 𝐴 ) = ⟨ 𝑋 , 𝑌 ⟩ ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) )
14	13	ad2antrl	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) ) → ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ↔ ( ( 1^st ‘ 𝐴 ) = ⟨ 𝑋 , 𝑌 ⟩ ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) )
15	9 14	mpbird	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) ) → 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ )
16		opelxpi	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑈 × 𝑉 ) )
17	16	3adant3	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑈 × 𝑉 ) )
18		simp3	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝑍 ∈ 𝑊 )
19	17 18	opelxpd	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) )
20	10 19	eqeltrid	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) )
21	20	adantr	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) )
22		eleq1	⊢ ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ → ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ↔ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ) )
23	22	adantl	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ↔ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ) )
24	21 23	mpbird	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) )
25		2fveq3	⊢ ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) ) )
26		ot1stg	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) ) = 𝑋 )
27	25 26	sylan9eqr	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 )
28		2fveq3	⊢ ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) ) )
29		ot2ndg	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) ) = 𝑌 )
30	28 29	sylan9eqr	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 )
31		fveq2	⊢ ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ → ( 2^nd ‘ 𝐴 ) = ( 2^nd ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) )
32		ot3rdg	⊢ ( 𝑍 ∈ 𝑊 → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) = 𝑍 )
33	32	3ad2ant3	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) = 𝑍 )
34	31 33	sylan9eqr	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → ( 2^nd ‘ 𝐴 ) = 𝑍 )
35	27 30 34	3jca	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) )
36	24 35	jca	⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) )
37	15 36	impbida	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑋 ∧ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑌 ∧ ( 2^nd ‘ 𝐴 ) = 𝑍 ) ) ↔ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) )

Metamath Proof Explorer

Theorem el2xptp0

Proof