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	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 ) , ( 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 ) ) } ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnmul	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		vp	$$setvarp$$
27		cvv	$$class\mathrm{V}$$
28		vm	$$setvarm$$
29	26	cv	$$setvarp$$
30	29 9	cfv	$$class{1}^{st}\left(p\right)$$
31		va	$$setvara$$
32	29 16	cfv	$$class{2}^{nd}\left(p\right)$$
33		vb	$$setvarb$$
34		vz	$$setvarz$$
35		vc	$$setvarc$$
36	31	cv	$$setvara$$
37		vd	$$setvard$$
38	33	cv	$$setvarb$$
39	35	cv	$$setvarc$$
40	28	cv	$$setvarm$$
41	39 38 40	co	$$class\left(cmb\right)$$
42		cnadd	$$class+$$
43	37	cv	$$setvard$$
44	36 43 40	co	$$class\left(amd\right)$$
45	41 44 42	co	$$class\left(\left(cmb\right)+\left(amd\right)\right)$$
46	34	cv	$$setvarz$$
47	39 43 40	co	$$class\left(cmd\right)$$
48	46 47 42	co	$$class\left(z+\left(cmd\right)\right)$$
49	45 48	wcel	$$wff\left(cmb\right)+\left(amd\right)\in \left(z+\left(cmd\right)\right)$$
50	49 37 38	wral	$$wff\forall d\in b\left(cmb\right)+\left(amd\right)\in \left(z+\left(cmd\right)\right)$$
51	50 35 36	wral	$$wff\forall c\in a\forall d\in b\left(cmb\right)+\left(amd\right)\in \left(z+\left(cmd\right)\right)$$
52	51 34 4	crab	$$class\left\{z\in \mathrm{On}|\forall c\in a\forall d\in b\left(cmb\right)+\left(amd\right)\in \left(z+\left(cmd\right)\right)\right\}$$
53	52	cint	$$class\bigcap \left\{z\in \mathrm{On}|\forall c\in a\forall d\in b\left(cmb\right)+\left(amd\right)\in \left(z+\left(cmd\right)\right)\right\}$$
54	33 32 53	csb	$$class⦋2^{nd}\left(p\right)/b⦌\bigcap \left\{z\in \mathrm{On}|\forall c\in a\forall d\in b\left(cmb\right)+\left(amd\right)\in \left(z+\left(cmd\right)\right)\right\}$$
55	31 30 54	csb	$$class⦋1^{st}\left(p\right)/a⦌⦋2^{nd}\left(p\right)/b⦌\bigcap \left\{z\in \mathrm{On}|\forall c\in a\forall d\in b\left(cmb\right)+\left(amd\right)\in \left(z+\left(cmd\right)\right)\right\}$$
56	26 28 27 27 55	cmpo	$$class\left(p\in \mathrm{V},m\in \mathrm{V}⟼⦋1^{st}\left(p\right)/a⦌⦋2^{nd}\left(p\right)/b⦌\bigcap \left\{z\in \mathrm{On}|\forall c\in a\forall d\in b\left(cmb\right)+\left(amd\right)\in \left(z+\left(cmd\right)\right)\right\}\right)$$
57	5 25 56	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(p\in \mathrm{V},m\in \mathrm{V}⟼⦋1^{st}\left(p\right)/a⦌⦋2^{nd}\left(p\right)/b⦌\bigcap \left\{z\in \mathrm{On}|\forall c\in a\forall d\in b\left(cmb\right)+\left(amd\right)\in \left(z+\left(cmd\right)\right)\right\}\right)\right)$$
58	0 57	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 ) , ( 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 ) ) } ) ) : 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 ) , ( 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 ) ) } ) ) with typecode wff