Metamath Proof Explorer

Definition df-nmul

Description: Define natural ordinal multiplication. This is the corresponding operation to df-nadd . (Contributed by Scott Fenton, 2-Jun-2026)

Ref Expression
Assertion df-nmul 
|- .no = frecs ( { <. x , y >. | ( x e. ( On X. On ) /\ y e. ( On X. On ) /\ ( ( ( 1st ` x ) _E ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) } , ( On X. On ) , ( p e. _V , m e. _V |-> [_ ( 1st ` p ) / a ]_ [_ ( 2nd ` p ) / b ]_ |^| { z e. On | A. c e. a A. d e. b ( ( c m b ) +no ( a m d ) ) e. ( z +no ( c m d ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnmul 
 |-  .no
1 vx 
 |-  x
2 vy 
 |-  y
3 1 cv 
 |-  x
4 con0 
 |-  On
5 4 4 cxp 
 |-  ( On X. On )
6 3 5 wcel 
 |-  x e. ( On X. On )
7 2 cv 
 |-  y
8 7 5 wcel 
 |-  y e. ( On X. On )
9 c1st 
 |-  1st
10 3 9 cfv 
 |-  ( 1st ` x )
11 cep 
 |-  _E
12 7 9 cfv 
 |-  ( 1st ` y )
13 10 12 11 wbr 
 |-  ( 1st ` x ) _E ( 1st ` y )
14 10 12 wceq 
 |-  ( 1st ` x ) = ( 1st ` y )
15 13 14 wo 
 |-  ( ( 1st ` x ) _E ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) )
16 c2nd 
 |-  2nd
17 3 16 cfv 
 |-  ( 2nd ` x )
18 7 16 cfv 
 |-  ( 2nd ` y )
19 17 18 11 wbr 
 |-  ( 2nd ` x ) _E ( 2nd ` y )
20 17 18 wceq 
 |-  ( 2nd ` x ) = ( 2nd ` y )
21 19 20 wo 
 |-  ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) )
22 3 7 wne 
 |-  x =/= y
23 15 21 22 w3a 
 |-  ( ( ( 1st ` x ) _E ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y )
24 6 8 23 w3a 
 |-  ( x e. ( On X. On ) /\ y e. ( On X. On ) /\ ( ( ( 1st ` x ) _E ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) )
25 24 1 2 copab 
 |-  { <. x , y >. | ( x e. ( On X. On ) /\ y e. ( On X. On ) /\ ( ( ( 1st ` x ) _E ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
26 vp 
 |-  p
27 cvv 
 |-  _V
28 vm 
 |-  m
29 26 cv 
 |-  p
30 29 9 cfv 
 |-  ( 1st ` p )
31 va 
 |-  a
32 29 16 cfv 
 |-  ( 2nd ` p )
33 vb 
 |-  b
34 vz 
 |-  z
35 vc 
 |-  c
36 31 cv 
 |-  a
37 vd 
 |-  d
38 33 cv 
 |-  b
39 35 cv 
 |-  c
40 28 cv 
 |-  m
41 39 38 40 co 
 |-  ( c m b )
42 cnadd 
 |-  +no
43 37 cv 
 |-  d
44 36 43 40 co 
 |-  ( a m d )
45 41 44 42 co 
 |-  ( ( c m b ) +no ( a m d ) )
46 34 cv 
 |-  z
47 39 43 40 co 
 |-  ( c m d )
48 46 47 42 co 
 |-  ( z +no ( c m d ) )
49 45 48 wcel 
 |-  ( ( c m b ) +no ( a m d ) ) e. ( z +no ( c m d ) )
50 49 37 38 wral 
 |-  A. d e. b ( ( c m b ) +no ( a m d ) ) e. ( z +no ( c m d ) )
51 50 35 36 wral 
 |-  A. c e. a A. d e. b ( ( c m b ) +no ( a m d ) ) e. ( z +no ( c m d ) )
52 51 34 4 crab 
 |-  { z e. On | A. c e. a A. d e. b ( ( c m b ) +no ( a m d ) ) e. ( z +no ( c m d ) ) }
53 52 cint 
 |-  |^| { z e. On | A. c e. a A. d e. b ( ( c m b ) +no ( a m d ) ) e. ( z +no ( c m d ) ) }
54 33 32 53 csb 
 |-  [_ ( 2nd ` p ) / b ]_ |^| { z e. On | A. c e. a A. d e. b ( ( c m b ) +no ( a m d ) ) e. ( z +no ( c m d ) ) }
55 31 30 54 csb 
 |-  [_ ( 1st ` p ) / a ]_ [_ ( 2nd ` p ) / b ]_ |^| { z e. On | A. c e. a A. d e. b ( ( c m b ) +no ( a m d ) ) e. ( z +no ( c m d ) ) }
56 26 28 27 27 55 cmpo 
 |-  ( p e. _V , m e. _V |-> [_ ( 1st ` p ) / a ]_ [_ ( 2nd ` p ) / b ]_ |^| { z e. On | A. c e. a A. d e. b ( ( c m b ) +no ( a m d ) ) e. ( z +no ( c m d ) ) } )
57 5 25 56 cfrecs 
 |-  frecs ( { <. x , y >. | ( x e. ( On X. On ) /\ y e. ( On X. On ) /\ ( ( ( 1st ` x ) _E ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) } , ( On X. On ) , ( p e. _V , m e. _V |-> [_ ( 1st ` p ) / a ]_ [_ ( 2nd ` p ) / b ]_ |^| { z e. On | A. c e. a A. d e. b ( ( c m b ) +no ( a m d ) ) e. ( z +no ( c m d ) ) } ) )
58 0 57 wceq 
 |-  .no = frecs ( { <. x , y >. | ( x e. ( On X. On ) /\ y e. ( On X. On ) /\ ( ( ( 1st ` x ) _E ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) } , ( On X. On ) , ( p e. _V , m e. _V |-> [_ ( 1st ` p ) / a ]_ [_ ( 2nd ` p ) / b ]_ |^| { z e. On | A. c e. a A. d e. b ( ( c m b ) +no ( a m d ) ) e. ( z +no ( c m d ) ) } ) )