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 XUYVZWAU×V×W1st1stA=X2nd1stA=Y2ndA=ZA=XYZ

Proof

Step Hyp Ref Expression
1 xp1st AU×V×W1stAU×V
2 1 ad2antrl XUYVZWAU×V×W1st1stA=X2nd1stA=Y2ndA=Z1stAU×V
3 3simpa 1st1stA=X2nd1stA=Y2ndA=Z1st1stA=X2nd1stA=Y
4 3 adantl AU×V×W1st1stA=X2nd1stA=Y2ndA=Z1st1stA=X2nd1stA=Y
5 4 adantl XUYVZWAU×V×W1st1stA=X2nd1stA=Y2ndA=Z1st1stA=X2nd1stA=Y
6 eqopi 1stAU×V1st1stA=X2nd1stA=Y1stA=XY
7 2 5 6 syl2anc XUYVZWAU×V×W1st1stA=X2nd1stA=Y2ndA=Z1stA=XY
8 simprr3 XUYVZWAU×V×W1st1stA=X2nd1stA=Y2ndA=Z2ndA=Z
9 7 8 jca XUYVZWAU×V×W1st1stA=X2nd1stA=Y2ndA=Z1stA=XY2ndA=Z
10 df-ot XYZ=XYZ
11 10 eqeq2i A=XYZA=XYZ
12 eqop AU×V×WA=XYZ1stA=XY2ndA=Z
13 11 12 bitrid AU×V×WA=XYZ1stA=XY2ndA=Z
14 13 ad2antrl XUYVZWAU×V×W1st1stA=X2nd1stA=Y2ndA=ZA=XYZ1stA=XY2ndA=Z
15 9 14 mpbird XUYVZWAU×V×W1st1stA=X2nd1stA=Y2ndA=ZA=XYZ
16 opelxpi XUYVXYU×V
17 16 3adant3 XUYVZWXYU×V
18 simp3 XUYVZWZW
19 17 18 opelxpd XUYVZWXYZU×V×W
20 10 19 eqeltrid XUYVZWXYZU×V×W
21 20 adantr XUYVZWA=XYZXYZU×V×W
22 eleq1 A=XYZAU×V×WXYZU×V×W
23 22 adantl XUYVZWA=XYZAU×V×WXYZU×V×W
24 21 23 mpbird XUYVZWA=XYZAU×V×W
25 2fveq3 A=XYZ1st1stA=1st1stXYZ
26 ot1stg XUYVZW1st1stXYZ=X
27 25 26 sylan9eqr XUYVZWA=XYZ1st1stA=X
28 2fveq3 A=XYZ2nd1stA=2nd1stXYZ
29 ot2ndg XUYVZW2nd1stXYZ=Y
30 28 29 sylan9eqr XUYVZWA=XYZ2nd1stA=Y
31 fveq2 A=XYZ2ndA=2ndXYZ
32 ot3rdg ZW2ndXYZ=Z
33 32 3ad2ant3 XUYVZW2ndXYZ=Z
34 31 33 sylan9eqr XUYVZWA=XYZ2ndA=Z
35 27 30 34 3jca XUYVZWA=XYZ1st1stA=X2nd1stA=Y2ndA=Z
36 24 35 jca XUYVZWA=XYZAU×V×W1st1stA=X2nd1stA=Y2ndA=Z
37 15 36 impbida XUYVZWAU×V×W1st1stA=X2nd1stA=Y2ndA=ZA=XYZ