This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ‘ 𝑦 ) ) )