Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-nadd Structured version   Visualization version   GIF version

Definition df-nadd 33588
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) ∧ (((1st𝑥) E (1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥) E (2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦))}, (On × On), (𝑧 ∈ V, 𝑎 ∈ V ↦ {𝑤 ∈ On ∣ ((𝑎 “ ({(1st𝑧)} × (2nd𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1st𝑧) × {(2nd𝑧)})) ⊆ 𝑤)}))
Distinct variable group:   𝑥,𝑦,𝑎,𝑧,𝑤

Detailed syntax breakdown of Definition df-nadd
StepHypRef Expression
1 cnadd 33587 . 2 class +no
2 con0 6231 . . . 4 class On
32, 2cxp 5564 . . 3 class (On × On)
4 vx . . . . . . 7 setvar 𝑥
54cv 1542 . . . . . 6 class 𝑥
65, 3wcel 2111 . . . . 5 wff 𝑥 ∈ (On × On)
7 vy . . . . . . 7 setvar 𝑦
87cv 1542 . . . . . 6 class 𝑦
98, 3wcel 2111 . . . . 5 wff 𝑦 ∈ (On × On)
10 c1st 7778 . . . . . . . . 9 class 1st
115, 10cfv 6398 . . . . . . . 8 class (1st𝑥)
128, 10cfv 6398 . . . . . . . 8 class (1st𝑦)
13 cep 5474 . . . . . . . 8 class E
1411, 12, 13wbr 5068 . . . . . . 7 wff (1st𝑥) E (1st𝑦)
1511, 12wceq 1543 . . . . . . 7 wff (1st𝑥) = (1st𝑦)
1614, 15wo 847 . . . . . 6 wff ((1st𝑥) E (1st𝑦) ∨ (1st𝑥) = (1st𝑦))
17 c2nd 7779 . . . . . . . . 9 class 2nd
185, 17cfv 6398 . . . . . . . 8 class (2nd𝑥)
198, 17cfv 6398 . . . . . . . 8 class (2nd𝑦)
2018, 19, 13wbr 5068 . . . . . . 7 wff (2nd𝑥) E (2nd𝑦)
2118, 19wceq 1543 . . . . . . 7 wff (2nd𝑥) = (2nd𝑦)
2220, 21wo 847 . . . . . 6 wff ((2nd𝑥) E (2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))
235, 8wne 2941 . . . . . 6 wff 𝑥𝑦
2416, 22, 23w3a 1089 . . . . 5 wff (((1st𝑥) E (1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥) E (2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦)
256, 9, 24w3a 1089 . . . 4 wff (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st𝑥) E (1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥) E (2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦))
2625, 4, 7copab 5130 . . 3 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st𝑥) E (1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥) E (2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦))}
27 vz . . . 4 setvar 𝑧
28 va . . . 4 setvar 𝑎
29 cvv 3421 . . . 4 class V
3028cv 1542 . . . . . . . . 9 class 𝑎
3127cv 1542 . . . . . . . . . . . 12 class 𝑧
3231, 10cfv 6398 . . . . . . . . . . 11 class (1st𝑧)
3332csn 4556 . . . . . . . . . 10 class {(1st𝑧)}
3431, 17cfv 6398 . . . . . . . . . 10 class (2nd𝑧)
3533, 34cxp 5564 . . . . . . . . 9 class ({(1st𝑧)} × (2nd𝑧))
3630, 35cima 5569 . . . . . . . 8 class (𝑎 “ ({(1st𝑧)} × (2nd𝑧)))
37 vw . . . . . . . . 9 setvar 𝑤
3837cv 1542 . . . . . . . 8 class 𝑤
3936, 38wss 3881 . . . . . . 7 wff (𝑎 “ ({(1st𝑧)} × (2nd𝑧))) ⊆ 𝑤
4034csn 4556 . . . . . . . . . 10 class {(2nd𝑧)}
4132, 40cxp 5564 . . . . . . . . 9 class ((1st𝑧) × {(2nd𝑧)})
4230, 41cima 5569 . . . . . . . 8 class (𝑎 “ ((1st𝑧) × {(2nd𝑧)}))
4342, 38wss 3881 . . . . . . 7 wff (𝑎 “ ((1st𝑧) × {(2nd𝑧)})) ⊆ 𝑤
4439, 43wa 399 . . . . . 6 wff ((𝑎 “ ({(1st𝑧)} × (2nd𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1st𝑧) × {(2nd𝑧)})) ⊆ 𝑤)
4544, 37, 2crab 3066 . . . . 5 class {𝑤 ∈ On ∣ ((𝑎 “ ({(1st𝑧)} × (2nd𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1st𝑧) × {(2nd𝑧)})) ⊆ 𝑤)}
4645cint 4874 . . . 4 class {𝑤 ∈ On ∣ ((𝑎 “ ({(1st𝑧)} × (2nd𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1st𝑧) × {(2nd𝑧)})) ⊆ 𝑤)}
4727, 28, 29, 29, 46cmpo 7234 . . 3 class (𝑧 ∈ V, 𝑎 ∈ V ↦ {𝑤 ∈ On ∣ ((𝑎 “ ({(1st𝑧)} × (2nd𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1st𝑧) × {(2nd𝑧)})) ⊆ 𝑤)})
483, 26, 47cfrecs 8043 . 2 class frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st𝑥) E (1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥) E (2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦))}, (On × On), (𝑧 ∈ V, 𝑎 ∈ V ↦ {𝑤 ∈ On ∣ ((𝑎 “ ({(1st𝑧)} × (2nd𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1st𝑧) × {(2nd𝑧)})) ⊆ 𝑤)}))
491, 48wceq 1543 1 wff +no = frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st𝑥) E (1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥) E (2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦))}, (On × On), (𝑧 ∈ V, 𝑎 ∈ V ↦ {𝑤 ∈ On ∣ ((𝑎 “ ({(1st𝑧)} × (2nd𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1st𝑧) × {(2nd𝑧)})) ⊆ 𝑤)}))
Colors of variables: wff setvar class
This definition is referenced by:  naddfn  33593  naddcllem  33594
  Copyright terms: Public domain W3C validator