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	Could not format assertion : No typesetting found for |- +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 ) } ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnadd	Could not format +no : No typesetting found for class +no with typecode class
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4		con0	$$class\mathrm{On}$$
5	4 4	cxp	$$class\left(\mathrm{On}\times \mathrm{On}\right)$$
6	3 5	wcel	$$wffx\in \left(\mathrm{On}\times \mathrm{On}\right)$$
7	2	cv	$$setvary$$
8	7 5	wcel	$$wffy\in \left(\mathrm{On}\times \mathrm{On}\right)$$
9		c1st	$$class{1}^{st}$$
10	3 9	cfv	$$class{1}^{st}\left(x\right)$$
11		cep	$$class\mathrm{E}$$
12	7 9	cfv	$$class{1}^{st}\left(y\right)$$
13	10 12 11	wbr	$$wff{1}^{st}\left(x\right)\mathrm{E}{1}^{st}\left(y\right)$$
14	10 12	wceq	$$wff{1}^{st}\left(x\right)=1^{st}\left(y\right)$$
15	13 14	wo	$$wff\left(1^{st}\left(x\right)\mathrm{E}{1}^{st}\left(y\right)\vee 1^{st}\left(x\right)=1^{st}\left(y\right)\right)$$
16		c2nd	$$class{2}^{nd}$$
17	3 16	cfv	$$class{2}^{nd}\left(x\right)$$
18	7 16	cfv	$$class{2}^{nd}\left(y\right)$$
19	17 18 11	wbr	$$wff{2}^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)$$
20	17 18	wceq	$$wff{2}^{nd}\left(x\right)=2^{nd}\left(y\right)$$
21	19 20	wo	$$wff\left(2^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)$$
22	3 7	wne	$$wffx\ne y$$
23	15 21 22	w3a	$$wff\left(\left(1^{st}\left(x\right)\mathrm{E}{1}^{st}\left(y\right)\vee 1^{st}\left(x\right)=1^{st}\left(y\right)\right)\wedge \left(2^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\wedge x\ne y\right)$$
24	6 8 23	w3a	$$wff\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge \left(\left(1^{st}\left(x\right)\mathrm{E}{1}^{st}\left(y\right)\vee 1^{st}\left(x\right)=1^{st}\left(y\right)\right)\wedge \left(2^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\wedge x\ne y\right)\right)$$
25	24 1 2	copab	$$class\left\{⟨x,y⟩|\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge \left(\left(1^{st}\left(x\right)\mathrm{E}{1}^{st}\left(y\right)\vee 1^{st}\left(x\right)=1^{st}\left(y\right)\right)\wedge \left(2^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\wedge x\ne y\right)\right)\right\}$$
26		vz	$$setvarz$$
27		cvv	$$class\mathrm{V}$$
28		va	$$setvara$$
29		vw	$$setvarw$$
30	28	cv	$$setvara$$
31	26	cv	$$setvarz$$
32	31 9	cfv	$$class{1}^{st}\left(z\right)$$
33	32	csn	$$class\left\{1^{st}\left(z\right)\right\}$$
34	31 16	cfv	$$class{2}^{nd}\left(z\right)$$
35	33 34	cxp	$$class\left(\left\{1^{st}\left(z\right)\right\}\times 2^{nd}\left(z\right)\right)$$
36	30 35	cima	$$classa\left[\left\{1^{st}\left(z\right)\right\}\times 2^{nd}\left(z\right)\right]$$
37	29	cv	$$setvarw$$
38	36 37	wss	$$wffa\left[\left\{1^{st}\left(z\right)\right\}\times 2^{nd}\left(z\right)\right]\subseteq w$$
39	34	csn	$$class\left\{2^{nd}\left(z\right)\right\}$$
40	32 39	cxp	$$class\left(1^{st}\left(z\right)\times \left\{2^{nd}\left(z\right)\right\}\right)$$
41	30 40	cima	$$classa\left[1^{st}\left(z\right)\times \left\{2^{nd}\left(z\right)\right\}\right]$$
42	41 37	wss	$$wffa\left[1^{st}\left(z\right)\times \left\{2^{nd}\left(z\right)\right\}\right]\subseteq w$$
43	38 42	wa	$$wff\left(a\left[\left\{1^{st}\left(z\right)\right\}\times 2^{nd}\left(z\right)\right]\subseteq w\wedge a\left[1^{st}\left(z\right)\times \left\{2^{nd}\left(z\right)\right\}\right]\subseteq w\right)$$
44	43 29 4	crab	$$class\left\{w\in \mathrm{On}|\left(a\left[\left\{1^{st}\left(z\right)\right\}\times 2^{nd}\left(z\right)\right]\subseteq w\wedge a\left[1^{st}\left(z\right)\times \left\{2^{nd}\left(z\right)\right\}\right]\subseteq w\right)\right\}$$
45	44	cint	$$class\bigcap \left\{w\in \mathrm{On}|\left(a\left[\left\{1^{st}\left(z\right)\right\}\times 2^{nd}\left(z\right)\right]\subseteq w\wedge a\left[1^{st}\left(z\right)\times \left\{2^{nd}\left(z\right)\right\}\right]\subseteq w\right)\right\}$$
46	26 28 27 27 45	cmpo	$$class\left(z\in \mathrm{V},a\in \mathrm{V}⟼\bigcap \left\{w\in \mathrm{On}|\left(a\left[\left\{1^{st}\left(z\right)\right\}\times 2^{nd}\left(z\right)\right]\subseteq w\wedge a\left[1^{st}\left(z\right)\times \left\{2^{nd}\left(z\right)\right\}\right]\subseteq w\right)\right\}\right)$$
47	5 25 46	cfrecs	$$class\mathrm{frecs}\left(\left\{⟨x,y⟩|\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge \left(\left(1^{st}\left(x\right)\mathrm{E}{1}^{st}\left(y\right)\vee 1^{st}\left(x\right)=1^{st}\left(y\right)\right)\wedge \left(2^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\wedge x\ne y\right)\right)\right\},\mathrm{On}\times \mathrm{On},\left(z\in \mathrm{V},a\in \mathrm{V}⟼\bigcap \left\{w\in \mathrm{On}|\left(a\left[\left\{1^{st}\left(z\right)\right\}\times 2^{nd}\left(z\right)\right]\subseteq w\wedge a\left[1^{st}\left(z\right)\times \left\{2^{nd}\left(z\right)\right\}\right]\subseteq w\right)\right\}\right)\right)$$
48	0 47	wceq	Could not format +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 ) } ) ) : No typesetting found for wff +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 ) } ) ) with typecode wff