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 leftno ⊢ y ∈ L ⁡ A → y ∈ No
6 5 adantr ⊢ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → y ∈ No
7 6 adantl ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → y ∈ No
8 onno ⊢ B ∈ On s → B ∈ No
9 8 adantl ⊢ A ∈ On s ∧ B ∈ On s → B ∈ No
10 9 adantr ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → B ∈ No
11 7 10 mulscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → y ⋅ s B ∈ No
12 onno ⊢ A ∈ On s → A ∈ No
13 12 adantr ⊢ A ∈ On s ∧ B ∈ On s → A ∈ No
14 13 adantr ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → A ∈ No
15 leftno ⊢ z ∈ L ⁡ B → z ∈ No
16 15 adantl ⊢ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → z ∈ No
17 16 adantl ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → z ∈ No
18 14 17 mulscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → A ⋅ s z ∈ No
19 11 18 addscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → y ⋅ s B + s A ⋅ s z ∈ No
20 7 17 mulscld ⊢ A ∈ On s ∧ B ∈ On s ∧ y ∈ L ⁡ A ∧ z ∈ L ⁡ B → y ⋅ s z ∈ No
21 19 20 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
22 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
23 21 22 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
24 23 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
25 24 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
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 2 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 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 25 56 elons2d ⊢ A ∈ On s ∧ B ∈ On s → A ⋅ s B ∈ On s