df-nadd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-nadd		Structured version Visualization version GIF version

Definition df-nadd 8687

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

**Assertion**
Ref	Expression
df-nadd	⊢ +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 ↦ ∩ {𝑤 ∈ On ∣ ((𝑎 “ ({(1^st ‘𝑧)} × (2^nd ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1^st ‘𝑧) × {(2^nd ‘𝑧)})) ⊆ 𝑤)}))

Distinct variable group: 𝑥,𝑦,𝑎,𝑧,𝑤

**Detailed syntax breakdown of Definition df-nadd**
Step	Hyp	Ref	Expression
1		cnadd 8686	. 2 class +no
2		con0 6365	. . . 4 class On
3	2, 2	cxp 5665	. . 3 class (On × On)
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1538	. . . . . 6 class 𝑥
6	5, 3	wcel 2107	. . . . 5 wff 𝑥 ∈ (On × On)
7		vy	. . . . . . 7 setvar 𝑦
8	7	cv 1538	. . . . . 6 class 𝑦
9	8, 3	wcel 2107	. . . . 5 wff 𝑦 ∈ (On × On)
10		c1st 7995	. . . . . . . . 9 class 1^st
11	5, 10	cfv 6542	. . . . . . . 8 class (1^st ‘𝑥)
12	8, 10	cfv 6542	. . . . . . . 8 class (1^st ‘𝑦)
13		cep 5565	. . . . . . . 8 class E
14	11, 12, 13	wbr 5125	. . . . . . 7 wff (1^st ‘𝑥) E (1^st ‘𝑦)
15	11, 12	wceq 1539	. . . . . . 7 wff (1^st ‘𝑥) = (1^st ‘𝑦)
16	14, 15	wo 847	. . . . . 6 wff ((1^st ‘𝑥) E (1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦))
17		c2nd 7996	. . . . . . . . 9 class 2^nd
18	5, 17	cfv 6542	. . . . . . . 8 class (2^nd ‘𝑥)
19	8, 17	cfv 6542	. . . . . . . 8 class (2^nd ‘𝑦)
20	18, 19, 13	wbr 5125	. . . . . . 7 wff (2^nd ‘𝑥) E (2^nd ‘𝑦)
21	18, 19	wceq 1539	. . . . . . 7 wff (2^nd ‘𝑥) = (2^nd ‘𝑦)
22	20, 21	wo 847	. . . . . 6 wff ((2^nd ‘𝑥) E (2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦))
23	5, 8	wne 2931	. . . . . 6 wff 𝑥 ≠ 𝑦
24	16, 22, 23	w3a 1086	. . . . 5 wff (((1^st ‘𝑥) E (1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥) E (2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦)
25	6, 9, 24	w3a 1086	. . . 4 wff (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1^st ‘𝑥) E (1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥) E (2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))
26	25, 4, 7	copab 5187	. . 3 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1^st ‘𝑥) E (1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥) E (2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
27		vz	. . . 4 setvar 𝑧
28		va	. . . 4 setvar 𝑎
29		cvv 3464	. . . 4 class V
30	28	cv 1538	. . . . . . . . 9 class 𝑎
31	27	cv 1538	. . . . . . . . . . . 12 class 𝑧
32	31, 10	cfv 6542	. . . . . . . . . . 11 class (1^st ‘𝑧)
33	32	csn 4608	. . . . . . . . . 10 class {(1^st ‘𝑧)}
34	31, 17	cfv 6542	. . . . . . . . . 10 class (2^nd ‘𝑧)
35	33, 34	cxp 5665	. . . . . . . . 9 class ({(1^st ‘𝑧)} × (2^nd ‘𝑧))
36	30, 35	cima 5670	. . . . . . . 8 class (𝑎 “ ({(1^st ‘𝑧)} × (2^nd ‘𝑧)))
37		vw	. . . . . . . . 9 setvar 𝑤
38	37	cv 1538	. . . . . . . 8 class 𝑤
39	36, 38	wss 3933	. . . . . . 7 wff (𝑎 “ ({(1^st ‘𝑧)} × (2^nd ‘𝑧))) ⊆ 𝑤
40	34	csn 4608	. . . . . . . . . 10 class {(2^nd ‘𝑧)}
41	32, 40	cxp 5665	. . . . . . . . 9 class ((1^st ‘𝑧) × {(2^nd ‘𝑧)})
42	30, 41	cima 5670	. . . . . . . 8 class (𝑎 “ ((1^st ‘𝑧) × {(2^nd ‘𝑧)}))
43	42, 38	wss 3933	. . . . . . 7 wff (𝑎 “ ((1^st ‘𝑧) × {(2^nd ‘𝑧)})) ⊆ 𝑤
44	39, 43	wa 395	. . . . . 6 wff ((𝑎 “ ({(1^st ‘𝑧)} × (2^nd ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1^st ‘𝑧) × {(2^nd ‘𝑧)})) ⊆ 𝑤)
45	44, 37, 2	crab 3420	. . . . 5 class {𝑤 ∈ On ∣ ((𝑎 “ ({(1^st ‘𝑧)} × (2^nd ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1^st ‘𝑧) × {(2^nd ‘𝑧)})) ⊆ 𝑤)}
46	45	cint 4928	. . . 4 class ∩ {𝑤 ∈ On ∣ ((𝑎 “ ({(1^st ‘𝑧)} × (2^nd ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1^st ‘𝑧) × {(2^nd ‘𝑧)})) ⊆ 𝑤)}
47	27, 28, 29, 29, 46	cmpo 7416	. . 3 class (𝑧 ∈ V, 𝑎 ∈ V ↦ ∩ {𝑤 ∈ On ∣ ((𝑎 “ ({(1^st ‘𝑧)} × (2^nd ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1^st ‘𝑧) × {(2^nd ‘𝑧)})) ⊆ 𝑤)})
48	3, 26, 47	cfrecs 8288	. 2 class 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 ↦ ∩ {𝑤 ∈ On ∣ ((𝑎 “ ({(1^st ‘𝑧)} × (2^nd ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1^st ‘𝑧) × {(2^nd ‘𝑧)})) ⊆ 𝑤)}))
49	1, 48	wceq 1539	1 wff +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 ↦ ∩ {𝑤 ∈ On ∣ ((𝑎 “ ({(1^st ‘𝑧)} × (2^nd ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1^st ‘𝑧) × {(2^nd ‘𝑧)})) ⊆ 𝑤)}))

Colors of variables: wff setvar class

This definition is referenced by: naddfn 8696 naddcllem 8697

W3C validator