Description: A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | relexpsucl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elnn0 | |
|
2 | simp3 | |
|
3 | simp1 | |
|
4 | relexpsucnnl | |
|
5 | 2 3 4 | syl2anc | |
6 | 5 | 3expib | |
7 | simp2 | |
|
8 | relcoi1 | |
|
9 | 7 8 | syl | |
10 | simp1 | |
|
11 | 10 | oveq2d | |
12 | simp3 | |
|
13 | relexp0 | |
|
14 | 12 7 13 | syl2anc | |
15 | 11 14 | eqtrd | |
16 | 15 | coeq2d | |
17 | 10 | oveq1d | |
18 | 0p1e1 | |
|
19 | 17 18 | eqtrdi | |
20 | 19 | oveq2d | |
21 | relexp1g | |
|
22 | 12 21 | syl | |
23 | 20 22 | eqtrd | |
24 | 9 16 23 | 3eqtr4rd | |
25 | 24 | 3expib | |
26 | 6 25 | jaoi | |
27 | 1 26 | sylbi | |
28 | 27 | 3impib | |
29 | 28 | 3com13 | |