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

Metamath Proof Explorer

Definition df-omul

Description: Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995)

Ref Expression
Assertion df-omul 
|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )

Detailed syntax breakdown

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