Definition df-nmul 36476

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

Assertion

Ref	Expression
df-nmul	⊢ ·no = frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), (𝑝 ∈ V, 𝑚 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑎⦌⦋(2nd ‘𝑝) / 𝑏⦌∩ {𝑧 ∈ On ∣ ∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))}))

Distinct variable group:   𝑥,𝑦,𝑧,𝑝,𝑚,𝑎,𝑏,𝑐,𝑑

Detailed syntax breakdown of Definition df-nmul

Step	Hyp	Ref	Expression
1		cnmul 36475	. 2 class ·no
2		con0 6331	. . . 4 class On
3	2, 2	cxp 5634	. . 3 class (On × On)
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1549	. . . . . 6 class 𝑥
6	5, 3	wcel 2132	. . . . 5 wff 𝑥 ∈ (On × On)
7		vy	. . . . . . 7 setvar 𝑦
8	7	cv 1549	. . . . . 6 class 𝑦
9	8, 3	wcel 2132	. . . . 5 wff 𝑦 ∈ (On × On)
10		c1st 7953	. . . . . . . . 9 class 1st
11	5, 10	cfv 6506	. . . . . . . 8 class (1st ‘𝑥)
12	8, 10	cfv 6506	. . . . . . . 8 class (1st ‘𝑦)
13		cep 5535	. . . . . . . 8 class E
14	11, 12, 13	wbr 5090	. . . . . . 7 wff (1st ‘𝑥) E (1st ‘𝑦)
15	11, 12	wceq 1550	. . . . . . 7 wff (1st ‘𝑥) = (1st ‘𝑦)
16	14, 15	wo 856	. . . . . 6 wff ((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦))
17		c2nd 7954	. . . . . . . . 9 class 2nd
18	5, 17	cfv 6506	. . . . . . . 8 class (2nd ‘𝑥)
19	8, 17	cfv 6506	. . . . . . . 8 class (2nd ‘𝑦)
20	18, 19, 13	wbr 5090	. . . . . . 7 wff (2nd ‘𝑥) E (2nd ‘𝑦)
21	18, 19	wceq 1550	. . . . . . 7 wff (2nd ‘𝑥) = (2nd ‘𝑦)
22	20, 21	wo 856	. . . . . 6 wff ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))
23	5, 8	wne 2947	. . . . . 6 wff 𝑥 ≠ 𝑦
24	16, 22, 23	w3a 1095	. . . . 5 wff (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦)
25	6, 9, 24	w3a 1095	. . . 4 wff (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))
26	25, 4, 7	copab 5152	. . 3 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
27		vp	. . . 4 setvar 𝑝
28		vm	. . . 4 setvar 𝑚
29		cvv 3444	. . . 4 class V
30		va	. . . . 5 setvar 𝑎
31	27	cv 1549	. . . . . 6 class 𝑝
32	31, 10	cfv 6506	. . . . 5 class (1st ‘𝑝)
33		vb	. . . . . 6 setvar 𝑏
34	31, 17	cfv 6506	. . . . . 6 class (2nd ‘𝑝)
35		vc	. . . . . . . . . . . . . 14 setvar 𝑐
36	35	cv 1549	. . . . . . . . . . . . 13 class 𝑐
37	33	cv 1549	. . . . . . . . . . . . 13 class 𝑏
38	28	cv 1549	. . . . . . . . . . . . 13 class 𝑚
39	36, 37, 38	co 7381	. . . . . . . . . . . 12 class (𝑐𝑚𝑏)
40	30	cv 1549	. . . . . . . . . . . . 13 class 𝑎
41		vd	. . . . . . . . . . . . . 14 setvar 𝑑
42	41	cv 1549	. . . . . . . . . . . . 13 class 𝑑
43	40, 42, 38	co 7381	. . . . . . . . . . . 12 class (𝑎𝑚𝑑)
44		cnadd 8619	. . . . . . . . . . . 12 class +no
45	39, 43, 44	co 7381	. . . . . . . . . . 11 class ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑))
46		vz	. . . . . . . . . . . . 13 setvar 𝑧
47	46	cv 1549	. . . . . . . . . . . 12 class 𝑧
48	36, 42, 38	co 7381	. . . . . . . . . . . 12 class (𝑐𝑚𝑑)
49	47, 48, 44	co 7381	. . . . . . . . . . 11 class (𝑧 +no (𝑐𝑚𝑑))
50	45, 49	wcel 2132	. . . . . . . . . 10 wff ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))
51	50, 41, 37	wral 3066	. . . . . . . . 9 wff ∀𝑑 ∈ 𝑏 ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))
52	51, 35, 40	wral 3066	. . . . . . . 8 wff ∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))
53	52, 46, 2	crab 3404	. . . . . . 7 class {𝑧 ∈ On ∣ ∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))}
54	53	cint 4895	. . . . . 6 class ∩ {𝑧 ∈ On ∣ ∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))}
55	33, 34, 54	csb 3843	. . . . 5 class ⦋(2nd ‘𝑝) / 𝑏⦌∩ {𝑧 ∈ On ∣ ∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))}
56	30, 32, 55	csb 3843	. . . 4 class ⦋(1st ‘𝑝) / 𝑎⦌⦋(2nd ‘𝑝) / 𝑏⦌∩ {𝑧 ∈ On ∣ ∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))}
57	27, 28, 29, 29, 56	cmpo 7383	. . 3 class (𝑝 ∈ V, 𝑚 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑎⦌⦋(2nd ‘𝑝) / 𝑏⦌∩ {𝑧 ∈ On ∣ ∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))})
58	3, 26, 57	cfrecs 8245	. 2 class frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), (𝑝 ∈ V, 𝑚 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑎⦌⦋(2nd ‘𝑝) / 𝑏⦌∩ {𝑧 ∈ On ∣ ∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))}))
59	1, 58	wceq 1550	1 wff ·no = frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), (𝑝 ∈ V, 𝑚 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑎⦌⦋(2nd ‘𝑝) / 𝑏⦌∩ {𝑧 ∈ On ∣ ∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))}))

This definition is referenced by:  nmulfn  36477  nmulprop  36478