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 leftssno ⊢ L ⁡ A ⊆ No
8 7 sseli ⊢ y ∈ L ⁡ A → y ∈ No
9 8 adantl ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A → y ∈ No
10 onsno ⊢ B ∈ On s → B ∈ No
11 10 ad2antlr ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A → B ∈ No
12 9 11 addscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A → y + s B ∈ No
13 eleq1 ⊢ x = y + s B → x ∈ No ↔ y + s B ∈ No
14 12 13 syl5ibrcom ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A → x = y + s B → x ∈ No
15 14 rexlimdva ⊢ A ∈ On s ∧ B ∈ On s → ∃ y ∈ L ⁡ A x = y + s B → x ∈ No
16 15 abssdv ⊢ A ∈ On s ∧ B ∈ On s → x | ∃ y ∈ L ⁡ A x = y + s B ⊆ No
17 onsno ⊢ A ∈ On s → A ∈ No
18 17 ad2antrr ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ B → A ∈ No
19 leftssno ⊢ L ⁡ B ⊆ No
20 19 sseli ⊢ y ∈ L ⁡ B → y ∈ No
21 20 adantl ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ B → y ∈ No
22 18 21 addscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ B → A + s y ∈ No
23 eleq1 ⊢ x = A + s y → x ∈ No ↔ A + s y ∈ No
24 22 23 syl5ibrcom ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ B → x = A + s y → x ∈ No
25 24 rexlimdva ⊢ A ∈ On s ∧ B ∈ On s → ∃ y ∈ L ⁡ B x = A + s y → x ∈ No
26 25 abssdv ⊢ A ∈ On s ∧ B ∈ On s → x | ∃ y ∈ L ⁡ B x = A + s y ⊆ No
27 16 26 unssd ⊢ A ∈ On s ∧ B ∈ On s → x | ∃ y ∈ L ⁡ A x = y + s B ∪ x | ∃ y ∈ L ⁡ B x = A + s y ⊆ No
28 1 elpw ⊢ L ⁡ A ∈ 𝒫 No ↔ L ⁡ A ⊆ No
29 7 28 mpbir ⊢ L ⁡ A ∈ 𝒫 No
30 nulssgt ⊢ L ⁡ A ∈ 𝒫 No → L ⁡ A ≪ s ∅
31 29 30 mp1i ⊢ A ∈ On s ∧ B ∈ On s → L ⁡ A ≪ s ∅
32 3 elpw ⊢ L ⁡ B ∈ 𝒫 No ↔ L ⁡ B ⊆ No
33 19 32 mpbir ⊢ L ⁡ B ∈ 𝒫 No
34 nulssgt ⊢ L ⁡ B ∈ 𝒫 No → L ⁡ B ≪ s ∅
35 33 34 mp1i ⊢ A ∈ On s ∧ B ∈ On s → L ⁡ B ≪ s ∅
36 onscutleft ⊢ A ∈ On s → A = L ⁡ A | s ∅
37 36 adantr ⊢ A ∈ On s ∧ B ∈ On s → A = L ⁡ A | s ∅
38 onscutleft ⊢ B ∈ On s → B = L ⁡ B | s ∅
39 38 adantl ⊢ A ∈ On s ∧ B ∈ On s → B = L ⁡ B | s ∅
40 31 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 27 49 elons2d ⊢ A ∈ On s ∧ B ∈ On s → A + s B ∈ On s