Description: Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fnoe | ⊢ ↑o Fn ( On × On ) |
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 ) |