Metamath Proof Explorer


Theorem fnoe

Description: Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion fnoe o Fn ( On × On )

Proof

Step Hyp Ref Expression
1 df-oexp o = ( 𝑥 ∈ On , 𝑦 ∈ On ↦ if ( 𝑥 = ∅ , ( 1o𝑦 ) , ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ·o 𝑥 ) ) , 1o ) ‘ 𝑦 ) ) )
2 1on 1o ∈ On
3 difexg ( 1o ∈ On → ( 1o𝑦 ) ∈ V )
4 2 3 ax-mp ( 1o𝑦 ) ∈ V
5 fvex ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ·o 𝑥 ) ) , 1o ) ‘ 𝑦 ) ∈ V
6 4 5 ifex if ( 𝑥 = ∅ , ( 1o𝑦 ) , ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ·o 𝑥 ) ) , 1o ) ‘ 𝑦 ) ) ∈ V
7 1 6 fnmpoi o Fn ( On × On )