Metamath Proof Explorer

Theorem fnoe

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

Ref Expression
Assertion fnoe ⊢ ↑ 𝑜 Fn On × On

Proof

Step Hyp Ref Expression
1 df-oexp ⊢ ↑ 𝑜 = x ∈ On , y ∈ On ⟼ if x = ∅ 1 𝑜 ∖ y rec ⁡ z ∈ V ⟼ z ⋅ 𝑜 x 1 𝑜 ⁡ y
2 1on ⊢ 1 𝑜 ∈ On
3 difexg ⊢ 1 𝑜 ∈ On → 1 𝑜 ∖ y ∈ V
4 2 3 ax-mp ⊢ 1 𝑜 ∖ y ∈ V
5 fvex ⊢ rec ⁡ z ∈ V ⟼ z ⋅ 𝑜 x 1 𝑜 ⁡ y ∈ V
6 4 5 ifex ⊢ if x = ∅ 1 𝑜 ∖ y rec ⁡ z ∈ V ⟼ z ⋅ 𝑜 x 1 𝑜 ⁡ y ∈ V
7 1 6 fnmpoi ⊢ ↑ 𝑜 Fn On × On