Description: Any positive power of a Cartesian product of non-disjoint sets is itself. (Contributed by RP, 13-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | relexpxpnnidm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 | |
|
2 | 1 | eqeq1d | |
3 | 2 | imbi2d | |
4 | oveq2 | |
|
5 | 4 | eqeq1d | |
6 | 5 | imbi2d | |
7 | oveq2 | |
|
8 | 7 | eqeq1d | |
9 | 8 | imbi2d | |
10 | oveq2 | |
|
11 | 10 | eqeq1d | |
12 | 11 | imbi2d | |
13 | 3simpa | |
|
14 | xpexg | |
|
15 | relexp1g | |
|
16 | 13 14 15 | 3syl | |
17 | simp2 | |
|
18 | 17 13 14 | 3syl | |
19 | simp1 | |
|
20 | relexpsucnnr | |
|
21 | 18 19 20 | syl2anc | |
22 | simp3 | |
|
23 | 22 | coeq1d | |
24 | simp23 | |
|
25 | 24 | xpcoidgend | |
26 | 21 23 25 | 3eqtrd | |
27 | 26 | 3exp | |
28 | 27 | a2d | |
29 | 3 6 9 12 16 28 | nnind | |