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
|- ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( ( A e. ( ( U X. V ) X. W ) /\ ( ( 1st ` ( 1st ` A ) ) = X /\ ( 2nd ` ( 1st ` A ) ) = Y /\ ( 2nd ` A ) = Z ) ) <-> A = <. X , Y , Z >. ) )

Proof

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