This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⋅ 𝑜 A 1 𝑜 ↾ ω ⁡ suc ⁡ B = x ∈ V ⟼ x ⋅ 𝑜 A ⁡ rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ↾ ω ⁡ B
3 peano2 ⊢ B ∈ ω → suc ⁡ B ∈ ω
4 3 fvresd ⊢ B ∈ ω → rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ↾ ω ⁡ suc ⁡ B = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ suc ⁡ B
5 fvres ⊢ B ∈ ω → rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ↾ ω ⁡ B = rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B
6 5 fveq2d ⊢ B ∈ ω → x ∈ V ⟼ x ⋅ 𝑜 A ⁡ rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ↾ ω ⁡ B = x ∈ V ⟼ x ⋅ 𝑜 A ⁡ rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B
7 2 4 6 3eqtr3d ⊢ B ∈ ω → rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ suc ⁡ B = x ∈ V ⟼ x ⋅ 𝑜 A ⁡ rec ⁡ x ∈ V ⟼ x ⋅ 𝑜 A 1 𝑜 ⁡ B
8 1 7 oesuclem ⊢ A ∈ On ∧ B ∈ ω → A ↑ 𝑜 suc ⁡ B = A ↑ 𝑜 B ⋅ 𝑜 A