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 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , ( 𝑝 ∈ V , 𝑚 ∈ V ↦ ⦋ ( 1^st ‘ 𝑝 ) / 𝑎 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑏 ⦌ ∩ { 𝑧 ∈ On ∣ ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( ( 𝑐 𝑚 𝑏 ) +no ( 𝑎 𝑚 𝑑 ) ) ∈ ( 𝑧 +no ( 𝑐 𝑚 𝑑 ) ) } ) )

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-nmul

Detailed syntax breakdown