Description: The value of Cartesian exponentiation at three. (Contributed by ML, 24-Oct-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | finxp3o | |- ( U ^^ 3o ) = ( ( U X. U ) X. U ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-3o | |- 3o = suc 2o |
|
| 2 | finxpeq2 | |- ( 3o = suc 2o -> ( U ^^ 3o ) = ( U ^^ suc 2o ) ) |
|
| 3 | 1 2 | ax-mp | |- ( U ^^ 3o ) = ( U ^^ suc 2o ) |
| 4 | 2onn | |- 2o e. _om |
|
| 5 | 2on0 | |- 2o =/= (/) |
|
| 6 | finxpsuc | |- ( ( 2o e. _om /\ 2o =/= (/) ) -> ( U ^^ suc 2o ) = ( ( U ^^ 2o ) X. U ) ) |
|
| 7 | 4 5 6 | mp2an | |- ( U ^^ suc 2o ) = ( ( U ^^ 2o ) X. U ) |
| 8 | finxp2o | |- ( U ^^ 2o ) = ( U X. U ) |
|
| 9 | 8 | xpeq1i | |- ( ( U ^^ 2o ) X. U ) = ( ( U X. U ) X. U ) |
| 10 | 3 7 9 | 3eqtri | |- ( U ^^ 3o ) = ( ( U X. U ) X. U ) |