Metamath Proof Explorer

Definition df-oexp

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

Ref Expression
Assertion df-oexp 
|- ^o = ( x e. On , y e. On |-> if ( x = (/) , ( 1o \ y ) , ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 coe 
 |-  ^o
1 vx 
 |-  x
2 con0 
 |-  On
3 vy 
 |-  y
4 1 cv 
 |-  x
5 c0 
 |-  (/)
6 4 5 wceq 
 |-  x = (/)
7 c1o 
 |-  1o
8 3 cv 
 |-  y
9 7 8 cdif 
 |-  ( 1o \ y )
10 vz 
 |-  z
11 cvv 
 |-  _V
12 10 cv 
 |-  z
13 comu 
 |-  .o
14 12 4 13 co 
 |-  ( z .o x )
15 10 11 14 cmpt 
 |-  ( z e. _V |-> ( z .o x ) )
16 15 7 crdg 
 |-  rec ( ( z e. _V |-> ( z .o x ) ) , 1o )
17 8 16 cfv 
 |-  ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y )
18 6 9 17 cif 
 |-  if ( x = (/) , ( 1o \ y ) , ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) )
19 1 3 2 2 18 cmpo 
 |-  ( x e. On , y e. On |-> if ( x = (/) , ( 1o \ y ) , ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) ) )
20 0 19 wceq 
 |-  ^o = ( x e. On , y e. On |-> if ( x = (/) , ( 1o \ y ) , ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) ) )