Definition df-oexp

Description: Define the ordinal exponentiation operation. (Contributed by NM, 30-Dec-2004)

	Ref	Expression
Assertion	df-oexp	⊢ ↑o = ( 𝑥 ∈ On , 𝑦 ∈ On ↦ if ( 𝑥 = ∅ , ( 1o ∖ 𝑦 ) , ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ·o 𝑥 ) ) , 1o ) ‘ 𝑦 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coe	⊢ ↑o
1		vx	⊢ 𝑥
2		con0	⊢ On
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑥
5		c0	⊢ ∅
6	4 5	wceq	⊢ 𝑥 = ∅
7		c1o	⊢ 1o
8	3	cv	⊢ 𝑦
9	7 8	cdif	⊢ ( 1o ∖ 𝑦 )
10		vz	⊢ 𝑧
11		cvv	⊢ V
12	10	cv	⊢ 𝑧
13		comu	⊢ ·o
14	12 4 13	co	⊢ ( 𝑧 ·o 𝑥 )
15	10 11 14	cmpt	⊢ ( 𝑧 ∈ V ↦ ( 𝑧 ·o 𝑥 ) )
16	15 7	crdg	⊢ rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ·o 𝑥 ) ) , 1o )
17	8 16	cfv	⊢ ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ·o 𝑥 ) ) , 1o ) ‘ 𝑦 )
18	6 9 17	cif	⊢ if ( 𝑥 = ∅ , ( 1o ∖ 𝑦 ) , ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ·o 𝑥 ) ) , 1o ) ‘ 𝑦 ) )
19	1 3 2 2 18	cmpo	⊢ ( 𝑥 ∈ On , 𝑦 ∈ On ↦ if ( 𝑥 = ∅ , ( 1o ∖ 𝑦 ) , ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ·o 𝑥 ) ) , 1o ) ‘ 𝑦 ) ) )
20	0 19	wceq	⊢ ↑o = ( 𝑥 ∈ On , 𝑦 ∈ On ↦ if ( 𝑥 = ∅ , ( 1o ∖ 𝑦 ) , ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ·o 𝑥 ) ) , 1o ) ‘ 𝑦 ) ) )