Metamath Proof Explorer

Theorem onmulscl

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

Ref Expression
Assertion onmulscl ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 ·s 𝐵 ) ∈ Ons )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( L ‘ 𝐴 ) ∈ V
2 fvex ⊢ ( L ‘ 𝐵 ) ∈ V
3 1 2 ab2rexex ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ∈ V
4 3 a1i ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ∈ V )
5 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
6 5 sseli ⊢ ( 𝑦 ∈ ( L ‘ 𝐴 ) → 𝑦 ∈ No )
7 6 adantr ⊢ ( ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) → 𝑦 ∈ No )
8 7 adantl ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → 𝑦 ∈ No )
9 onsno ⊢ ( 𝐵 ∈ Ons → 𝐵 ∈ No )
10 9 adantl ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐵 ∈ No )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → 𝐵 ∈ No )
12 8 11 mulscld ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑦 ·s 𝐵 ) ∈ No )
13 onsno ⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )
14 13 adantr ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐴 ∈ No )
15 14 adantr ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → 𝐴 ∈ No )
16 leftssno ⊢ ( L ‘ 𝐵 ) ⊆ No
17 16 sseli ⊢ ( 𝑧 ∈ ( L ‘ 𝐵 ) → 𝑧 ∈ No )
18 17 adantl ⊢ ( ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) → 𝑧 ∈ No )
19 18 adantl ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → 𝑧 ∈ No )
20 15 19 mulscld ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝐴 ·s 𝑧 ) ∈ No )
21 12 20 addscld ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) ∈ No )
22 8 19 mulscld ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑦 ·s 𝑧 ) ∈ No )
23 21 22 subscld ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ∈ No )
24 eleq1 ⊢ ( 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) → ( 𝑥 ∈ No ↔ ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ∈ No ) )
25 23 24 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) → 𝑥 ∈ No ) )
26 25 rexlimdvva ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) → 𝑥 ∈ No ) )
27 26 abssdv ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ⊆ No )
28 1 elpw ⊢ ( ( L ‘ 𝐴 ) ∈ 𝒫 No ↔ ( L ‘ 𝐴 ) ⊆ No )
29 5 28 mpbir ⊢ ( L ‘ 𝐴 ) ∈ 𝒫 No
30 nulssgt ⊢ ( ( L ‘ 𝐴 ) ∈ 𝒫 No → ( L ‘ 𝐴 ) <<s ∅ )
31 29 30 mp1i ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( L ‘ 𝐴 ) <<s ∅ )
32 2 elpw ⊢ ( ( L ‘ 𝐵 ) ∈ 𝒫 No ↔ ( L ‘ 𝐵 ) ⊆ No )
33 16 32 mpbir ⊢ ( L ‘ 𝐵 ) ∈ 𝒫 No
34 nulssgt ⊢ ( ( L ‘ 𝐵 ) ∈ 𝒫 No → ( L ‘ 𝐵 ) <<s ∅ )
35 33 34 mp1i ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( L ‘ 𝐵 ) <<s ∅ )
36 onscutleft ⊢ ( 𝐴 ∈ Ons → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
37 36 adantr ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
38 onscutleft ⊢ ( 𝐵 ∈ Ons → 𝐵 = ( ( L ‘ 𝐵 ) |s ∅ ) )
39 38 adantl ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐵 = ( ( L ‘ 𝐵 ) |s ∅ ) )
40 31 35 37 39 mulsunif ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 ·s 𝐵 ) = ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ) ) )
41 rex0 ⊢ ¬ ∃ 𝑦 ∈ ∅ ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) )
42 41 abf ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } = ∅
43 42 uneq2i ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ) = ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ∪ ∅ )
44 un0 ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ∪ ∅ ) = { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) }
45 43 44 eqtri ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ) = { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) }
46 rex0 ⊢ ¬ ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) )
47 46 a1i ⊢ ( 𝑦 ∈ ( L ‘ 𝐴 ) → ¬ ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) )
48 47 nrex ⊢ ¬ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) )
49 48 abf ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } = ∅
50 rex0 ⊢ ¬ ∃ 𝑦 ∈ ∅ ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) )
51 50 abf ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } = ∅
52 49 51 uneq12i ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ) = ( ∅ ∪ ∅ )
53 un0 ⊢ ( ∅ ∪ ∅ ) = ∅
54 52 53 eqtri ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ) = ∅
55 45 54 oveq12i ⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ∅ 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ) ) = ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } |s ∅ )
56 40 55 eqtrdi ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 ·s 𝐵 ) = ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } |s ∅ ) )
57 4 27 56 elons2d ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 ·s 𝐵 ) ∈ Ons )