Metamath Proof Explorer

Theorem onesuc

Description: Exponentiation with a successor exponent. Definition 8.30 of TakeutiZaring p. 67. (Contributed by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion onesuc ⊢A∈On∧B∈ω→A↑𝑜suc⁡B=A↑𝑜B⋅𝑜A

Proof

Step Hyp Ref Expression
1 limom ⊢Lim⁡ω
2 frsuc ⊢B∈ω→rec⁡x∈V⟼x⋅𝑜A1𝑜↾ω⁡suc⁡B=x∈V⟼x⋅𝑜A⁡rec⁡x∈V⟼x⋅𝑜A1𝑜↾ω⁡B
3 peano2 ⊢B∈ω→suc⁡B∈ω
4 3 fvresd ⊢B∈ω→rec⁡x∈V⟼x⋅𝑜A1𝑜↾ω⁡suc⁡B=rec⁡x∈V⟼x⋅𝑜A1𝑜⁡suc⁡B
5 fvres ⊢B∈ω→rec⁡x∈V⟼x⋅𝑜A1𝑜↾ω⁡B=rec⁡x∈V⟼x⋅𝑜A1𝑜⁡B
6 5 fveq2d ⊢B∈ω→x∈V⟼x⋅𝑜A⁡rec⁡x∈V⟼x⋅𝑜A1𝑜↾ω⁡B=x∈V⟼x⋅𝑜A⁡rec⁡x∈V⟼x⋅𝑜A1𝑜⁡B
7 2 4 6 3eqtr3d ⊢B∈ω→rec⁡x∈V⟼x⋅𝑜A1𝑜⁡suc⁡B=x∈V⟼x⋅𝑜A⁡rec⁡x∈V⟼x⋅𝑜A1𝑜⁡B
8 1 7 oesuclem ⊢A∈On∧B∈ω→A↑𝑜suc⁡B=A↑𝑜B⋅𝑜A