Metamath Proof Explorer


Theorem finxpsuc

Description: The value of Cartesian exponentiation at a successor. (Contributed by ML, 24-Oct-2020)

Ref Expression
Assertion finxpsuc N ω N U ↑↑ suc N = U ↑↑ N × U

Proof

Step Hyp Ref Expression
1 nnord N ω Ord N
2 ordge1n0 Ord N 1 𝑜 N N
3 1 2 syl N ω 1 𝑜 N N
4 3 biimprd N ω N 1 𝑜 N
5 4 imdistani N ω N N ω 1 𝑜 N
6 eqid y ω , x V if y = 1 𝑜 x U if x V × U y 1 st x y x = y ω , x V if y = 1 𝑜 x U if x V × U y 1 st x y x
7 6 finxpsuclem N ω 1 𝑜 N U ↑↑ suc N = U ↑↑ N × U
8 5 7 syl N ω N U ↑↑ suc N = U ↑↑ N × U