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 )