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 >. ) )