Metamath Proof Explorer

Theorem onmulscl

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

Ref Expression
Assertion onmulscl ⊢ A ∈ On s ∧ B ∈ On s → A ⋅ s B ∈ On s

Proof

Step Hyp Ref Expression
1 fvex ⊢ L ⁡ A ∈ V
2 fvex ⊢ L ⁡ B ∈ V
3 1 2 ab2rexex ⊢ x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∈ V
4 3 a1i ⊢ A ∈ On s ∧ B ∈ On s → x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∈ V
5 leftssno ⊢ L ⁡ A ⊆ No
6 5 sseli ⊢ y ∈ L ⁡ A → y ∈ No
7 6 adantr ⊢ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → y ∈ No
8 7 adantl ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → y ∈ No
9 onsno ⊢ B ∈ On s → B ∈ No
10 9 adantl ⊢ A ∈ On s ∧ B ∈ On s → B ∈ No
11 10 adantr ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → B ∈ No
12 8 11 mulscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → y ⋅ s B ∈ No
13 onsno ⊢ A ∈ On s → A ∈ No
14 13 adantr ⊢ A ∈ On s ∧ B ∈ On s → A ∈ No
15 14 adantr ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → A ∈ No
16 leftssno ⊢ L ⁡ B ⊆ No
17 16 sseli ⊢ z ∈ L ⁡ B → z ∈ No
18 17 adantl ⊢ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → z ∈ No
19 18 adantl ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → z ∈ No
20 15 19 mulscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → A ⋅ s z ∈ No
21 12 20 addscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → y ⋅ s B + s A ⋅ s z ∈ No
22 8 19 mulscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → y ⋅ s z ∈ No
23 21 22 subscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∈ No
24 eleq1 ⊢ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z → x ∈ No ↔ y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∈ No
25 23 24 syl5ibrcom ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z → x ∈ No
26 25 rexlimdvva ⊢ A ∈ On s ∧ B ∈ On s → ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z → x ∈ No
27 26 abssdv ⊢ A ∈ On s ∧ B ∈ On s → x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ⊆ No
28 1 elpw ⊢ L ⁡ A ∈ 𝒫 No ↔ L ⁡ A ⊆ No
29 5 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 2 elpw ⊢ L ⁡ B ∈ 𝒫 No ↔ L ⁡ B ⊆ No
33 16 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 mulsunif ⊢ A ∈ On s ∧ B ∈ On s → A ⋅ s B = x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∪ x | ∃ y ∈ ∅ ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z | s x | ∃ y ∈ L ⁡ A ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∪ x | ∃ y ∈ ∅ ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z
41 rex0 ⊢ ¬ ∃ y ∈ ∅ ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z
42 41 abf ⊢ x | ∃ y ∈ ∅ ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z = ∅
43 42 uneq2i ⊢ x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∪ x | ∃ y ∈ ∅ ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z = x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∪ ∅
44 un0 ⊢ x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∪ ∅ = x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z
45 43 44 eqtri ⊢ x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∪ x | ∃ y ∈ ∅ ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z = x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z
46 rex0 ⊢ ¬ ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z
47 46 a1i ⊢ y ∈ L ⁡ A → ¬ ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z
48 47 nrex ⊢ ¬ ∃ y ∈ L ⁡ A ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z
49 48 abf ⊢ x | ∃ y ∈ L ⁡ A ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z = ∅
50 rex0 ⊢ ¬ ∃ y ∈ ∅ ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z
51 50 abf ⊢ x | ∃ y ∈ ∅ ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z = ∅
52 49 51 uneq12i ⊢ x | ∃ y ∈ L ⁡ A ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∪ x | ∃ y ∈ ∅ ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z = ∅ ∪ ∅
53 un0 ⊢ ∅ ∪ ∅ = ∅
54 52 53 eqtri ⊢ x | ∃ y ∈ L ⁡ A ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∪ x | ∃ y ∈ ∅ ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z = ∅
55 45 54 oveq12i ⊢ x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∪ x | ∃ y ∈ ∅ ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z | s x | ∃ y ∈ L ⁡ A ∃ z ∈ ∅ x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z ∪ x | ∃ y ∈ ∅ ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z = x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z | s ∅
56 40 55 eqtrdi ⊢ A ∈ On s ∧ B ∈ On s → A ⋅ s B = x | ∃ y ∈ L ⁡ A ∃ z ∈ L ⁡ B x = y ⋅ s B + s A ⋅ s z - s y ⋅ s z | s ∅
57 4 27 56 elons2d ⊢ A ∈ On s ∧ B ∈ On s → A ⋅ s B ∈ On s