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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xp1st | |
|
2 | 1 | ad2antrl | |
3 | 3simpa | |
|
4 | 3 | adantl | |
5 | 4 | adantl | |
6 | eqopi | |
|
7 | 2 5 6 | syl2anc | |
8 | simprr3 | |
|
9 | 7 8 | jca | |
10 | df-ot | |
|
11 | 10 | eqeq2i | |
12 | eqop | |
|
13 | 11 12 | bitrid | |
14 | 13 | ad2antrl | |
15 | 9 14 | mpbird | |
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 | |
|
26 | ot1stg | |
|
27 | 25 26 | sylan9eqr | |
28 | 2fveq3 | |
|
29 | ot2ndg | |
|
30 | 28 29 | sylan9eqr | |
31 | fveq2 | |
|
32 | ot3rdg | |
|
33 | 32 | 3ad2ant3 | |
34 | 31 33 | sylan9eqr | |
35 | 27 30 34 | 3jca | |
36 | 24 35 | jca | |
37 | 15 36 | impbida | |