Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 xp1st ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) → ( 1st𝐴 ) ∈ ( 𝑈 × 𝑉 ) )
2 1 ad2antrl ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ∧ ( 2nd𝐴 ) = 𝑍 ) ) ) → ( 1st𝐴 ) ∈ ( 𝑈 × 𝑉 ) )
3 3simpa ( ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ∧ ( 2nd𝐴 ) = 𝑍 ) → ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ) )
4 3 adantl ( ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ∧ ( 2nd𝐴 ) = 𝑍 ) ) → ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ) )
5 4 adantl ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ∧ ( 2nd𝐴 ) = 𝑍 ) ) ) → ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ) )
6 eqopi ( ( ( 1st𝐴 ) ∈ ( 𝑈 × 𝑉 ) ∧ ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ) ) → ( 1st𝐴 ) = ⟨ 𝑋 , 𝑌 ⟩ )
7 2 5 6 syl2anc ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ∧ ( 2nd𝐴 ) = 𝑍 ) ) ) → ( 1st𝐴 ) = ⟨ 𝑋 , 𝑌 ⟩ )
8 simprr3 ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ∧ ( 2nd𝐴 ) = 𝑍 ) ) ) → ( 2nd𝐴 ) = 𝑍 )
9 7 8 jca ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ∧ ( 2nd𝐴 ) = 𝑍 ) ) ) → ( ( 1st𝐴 ) = ⟨ 𝑋 , 𝑌 ⟩ ∧ ( 2nd𝐴 ) = 𝑍 ) )
10 df-ot 𝑋 , 𝑌 , 𝑍 ⟩ = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍
11 10 eqeq2i ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ↔ 𝐴 = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ )
12 eqop ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) → ( 𝐴 = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ↔ ( ( 1st𝐴 ) = ⟨ 𝑋 , 𝑌 ⟩ ∧ ( 2nd𝐴 ) = 𝑍 ) ) )
13 11 12 syl5bb ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) → ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ↔ ( ( 1st𝐴 ) = ⟨ 𝑋 , 𝑌 ⟩ ∧ ( 2nd𝐴 ) = 𝑍 ) ) )
14 13 ad2antrl ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ∧ ( 2nd𝐴 ) = 𝑍 ) ) ) → ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ↔ ( ( 1st𝐴 ) = ⟨ 𝑋 , 𝑌 ⟩ ∧ ( 2nd𝐴 ) = 𝑍 ) ) )
15 9 14 mpbird ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ∧ ( 2nd𝐴 ) = 𝑍 ) ) ) → 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ )
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 ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ → ( 1st ‘ ( 1st𝐴 ) ) = ( 1st ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) ) )
26 ot1stg ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) → ( 1st ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) ) = 𝑋 )
27 25 26 sylan9eqr ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 )
28 2fveq3 ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ → ( 2nd ‘ ( 1st𝐴 ) ) = ( 2nd ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) ) )
29 ot2ndg ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) → ( 2nd ‘ ( 1st ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) ) = 𝑌 )
30 28 29 sylan9eqr ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 )
31 fveq2 ( 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ → ( 2nd𝐴 ) = ( 2nd ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) )
32 ot3rdg ( 𝑍𝑊 → ( 2nd ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) = 𝑍 )
33 32 3ad2ant3 ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) → ( 2nd ‘ ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) = 𝑍 )
34 31 33 sylan9eqr ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → ( 2nd𝐴 ) = 𝑍 )
35 27 30 34 3jca ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ∧ ( 2nd𝐴 ) = 𝑍 ) )
36 24 35 jca ( ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) ∧ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) → ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ∧ ( 2nd𝐴 ) = 𝑍 ) ) )
37 15 36 impbida ( ( 𝑋𝑈𝑌𝑉𝑍𝑊 ) → ( ( 𝐴 ∈ ( ( 𝑈 × 𝑉 ) × 𝑊 ) ∧ ( ( 1st ‘ ( 1st𝐴 ) ) = 𝑋 ∧ ( 2nd ‘ ( 1st𝐴 ) ) = 𝑌 ∧ ( 2nd𝐴 ) = 𝑍 ) ) ↔ 𝐴 = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) )