Metamath Proof Explorer

Definition df-nadd

Description: Define natural ordinal addition. This is a commutative form of addition over the ordinals. (Contributed by Scott Fenton, 26-Aug-2024)

Ref Expression
Assertion df-nadd 
|- +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 ) , ( z e. _V , a e. _V |-> |^| { w e. On | ( ( a " ( { ( 1st ` z ) } X. ( 2nd ` z ) ) ) C_ w /\ ( a " ( ( 1st ` z ) X. { ( 2nd ` z ) } ) ) C_ w ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnadd 
 |-  +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 vz 
 |-  z
27 cvv 
 |-  _V
28 va 
 |-  a
29 vw 
 |-  w
30 28 cv 
 |-  a
31 26 cv 
 |-  z
32 31 9 cfv 
 |-  ( 1st ` z )
33 32 csn 
 |-  { ( 1st ` z ) }
34 31 16 cfv 
 |-  ( 2nd ` z )
35 33 34 cxp 
 |-  ( { ( 1st ` z ) } X. ( 2nd ` z ) )
36 30 35 cima 
 |-  ( a " ( { ( 1st ` z ) } X. ( 2nd ` z ) ) )
37 29 cv 
 |-  w
38 36 37 wss 
 |-  ( a " ( { ( 1st ` z ) } X. ( 2nd ` z ) ) ) C_ w
39 34 csn 
 |-  { ( 2nd ` z ) }
40 32 39 cxp 
 |-  ( ( 1st ` z ) X. { ( 2nd ` z ) } )
41 30 40 cima 
 |-  ( a " ( ( 1st ` z ) X. { ( 2nd ` z ) } ) )
42 41 37 wss 
 |-  ( a " ( ( 1st ` z ) X. { ( 2nd ` z ) } ) ) C_ w
43 38 42 wa 
 |-  ( ( a " ( { ( 1st ` z ) } X. ( 2nd ` z ) ) ) C_ w /\ ( a " ( ( 1st ` z ) X. { ( 2nd ` z ) } ) ) C_ w )
44 43 29 4 crab 
 |-  { w e. On | ( ( a " ( { ( 1st ` z ) } X. ( 2nd ` z ) ) ) C_ w /\ ( a " ( ( 1st ` z ) X. { ( 2nd ` z ) } ) ) C_ w ) }
45 44 cint 
 |-  |^| { w e. On | ( ( a " ( { ( 1st ` z ) } X. ( 2nd ` z ) ) ) C_ w /\ ( a " ( ( 1st ` z ) X. { ( 2nd ` z ) } ) ) C_ w ) }
46 26 28 27 27 45 cmpo 
 |-  ( z e. _V , a e. _V |-> |^| { w e. On | ( ( a " ( { ( 1st ` z ) } X. ( 2nd ` z ) ) ) C_ w /\ ( a " ( ( 1st ` z ) X. { ( 2nd ` z ) } ) ) C_ w ) } )
47 5 25 46 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 ) , ( z e. _V , a e. _V |-> |^| { w e. On | ( ( a " ( { ( 1st ` z ) } X. ( 2nd ` z ) ) ) C_ w /\ ( a " ( ( 1st ` z ) X. { ( 2nd ` z ) } ) ) C_ w ) } ) )
48 0 47 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 ) , ( z e. _V , a e. _V |-> |^| { w e. On | ( ( a " ( { ( 1st ` z ) } X. ( 2nd ` z ) ) ) C_ w /\ ( a " ( ( 1st ` z ) X. { ( 2nd ` z ) } ) ) C_ w ) } ) )