Metamath Proof Explorer

Theorem onaddscl

Description: The surreal ordinals are closed under addition. (Contributed by Scott Fenton, 22-Aug-2025)

Ref Expression
Assertion onaddscl ⊢ A ∈ On s ∧ B ∈ On s → A + s B ∈ On s

Proof

Step Hyp Ref Expression
1 fvex ⊢ L ⁡ A ∈ V
2 1 abrexex ⊢ x | ∃ y ∈ L ⁡ A x = y + s B ∈ V
3 fvex ⊢ L ⁡ B ∈ V
4 3 abrexex ⊢ x | ∃ y ∈ L ⁡ B x = A + s y ∈ V
5 2 4 unex ⊢ x | ∃ y ∈ L ⁡ A x = y + s B ∪ x | ∃ y ∈ L ⁡ B x = A + s y ∈ V
6 5 a1i ⊢ A ∈ On s ∧ B ∈ On s → x | ∃ y ∈ L ⁡ A x = y + s B ∪ x | ∃ y ∈ L ⁡ B x = A + s y ∈ V
7 leftno ⊢ y ∈ L ⁡ A → y ∈ No
8 7 adantl ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A → y ∈ No
9 onno ⊢ B ∈ On s → B ∈ No
10 9 ad2antlr ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A → B ∈ No
11 8 10 addscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A → y + s B ∈ No
12 eleq1 ⊢ x = y + s B → x ∈ No ↔ y + s B ∈ No
13 11 12 syl5ibrcom ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A → x = y + s B → x ∈ No
14 13 rexlimdva ⊢ A ∈ On s ∧ B ∈ On s → ∃ y ∈ L ⁡ A x = y + s B → x ∈ No
15 14 abssdv ⊢ A ∈ On s ∧ B ∈ On s → x | ∃ y ∈ L ⁡ A x = y + s B ⊆ No
16 onno ⊢ A ∈ On s → A ∈ No
17 16 ad2antrr ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ B → A ∈ No
18 leftno ⊢ y ∈ L ⁡ B → y ∈ No
19 18 adantl ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ B → y ∈ No
20 17 19 addscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ B → A + s y ∈ No
21 eleq1 ⊢ x = A + s y → x ∈ No ↔ A + s y ∈ No
22 20 21 syl5ibrcom ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ B → x = A + s y → x ∈ No
23 22 rexlimdva ⊢ A ∈ On s ∧ B ∈ On s → ∃ y ∈ L ⁡ B x = A + s y → x ∈ No
24 23 abssdv ⊢ A ∈ On s ∧ B ∈ On s → x | ∃ y ∈ L ⁡ B x = A + s y ⊆ No
25 15 24 unssd ⊢ A ∈ On s ∧ B ∈ On s → x | ∃ y ∈ L ⁡ A x = y + s B ∪ x | ∃ y ∈ L ⁡ B x = A + s y ⊆ No
26 leftssno ⊢ L ⁡ A ⊆ No
27 1 elpw ⊢ L ⁡ A ∈ 𝒫 No ↔ L ⁡ A ⊆ No
28 26 27 mpbir ⊢ L ⁡ A ∈ 𝒫 No
29 nulsgts ⊢ L ⁡ A ∈ 𝒫 No → L ⁡ A ≪ s ∅
30 28 29 mp1i ⊢ A ∈ On s ∧ B ∈ On s → L ⁡ A ≪ s ∅
31 leftssno ⊢ L ⁡ B ⊆ No
32 3 elpw ⊢ L ⁡ B ∈ 𝒫 No ↔ L ⁡ B ⊆ No
33 31 32 mpbir ⊢ L ⁡ B ∈ 𝒫 No
34 nulsgts ⊢ L ⁡ B ∈ 𝒫 No → L ⁡ B ≪ s ∅
35 33 34 mp1i ⊢ A ∈ On s ∧ B ∈ On s → L ⁡ B ≪ s ∅
36 oncutleft ⊢ A ∈ On s → A = L ⁡ A | s ∅
37 36 adantr ⊢ A ∈ On s ∧ B ∈ On s → A = L ⁡ A | s ∅
38 oncutleft ⊢ B ∈ On s → B = L ⁡ B | s ∅
39 38 adantl ⊢ A ∈ On s ∧ B ∈ On s → B = L ⁡ B | s ∅
40 30 35 37 39 addsunif ⊢ A ∈ On s ∧ B ∈ On s → A + s B = x | ∃ y ∈ L ⁡ A x = y + s B ∪ x | ∃ y ∈ L ⁡ B x = A + s y | s x | ∃ y ∈ ∅ x = y + s B ∪ x | ∃ y ∈ ∅ x = A + s y
41 rex0 ⊢ ¬ ∃ y ∈ ∅ x = y + s B
42 41 abf ⊢ x | ∃ y ∈ ∅ x = y + s B = ∅
43 rex0 ⊢ ¬ ∃ y ∈ ∅ x = A + s y
44 43 abf ⊢ x | ∃ y ∈ ∅ x = A + s y = ∅
45 42 44 uneq12i ⊢ x | ∃ y ∈ ∅ x = y + s B ∪ x | ∃ y ∈ ∅ x = A + s y = ∅ ∪ ∅
46 un0 ⊢ ∅ ∪ ∅ = ∅
47 45 46 eqtri ⊢ x | ∃ y ∈ ∅ x = y + s B ∪ x | ∃ y ∈ ∅ x = A + s y = ∅
48 47 oveq2i ⊢ x | ∃ y ∈ L ⁡ A x = y + s B ∪ x | ∃ y ∈ L ⁡ B x = A + s y | s x | ∃ y ∈ ∅ x = y + s B ∪ x | ∃ y ∈ ∅ x = A + s y = x | ∃ y ∈ L ⁡ A x = y + s B ∪ x | ∃ y ∈ L ⁡ B x = A + s y | s ∅
49 40 48 eqtrdi ⊢ A ∈ On s ∧ B ∈ On s → A + s B = x | ∃ y ∈ L ⁡ A x = y + s B ∪ x | ∃ y ∈ L ⁡ B x = A + s y | s ∅
50 6 25 49 elons2d ⊢ A ∈ On s ∧ B ∈ On s → A + s B ∈ On s