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 leftno ⊢ ( 𝑦 ∈ ( L ‘ 𝐴 ) → 𝑦 ∈ No )
6 5 adantr ⊢ ( ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) → 𝑦 ∈ No )
7 6 adantl ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → 𝑦 ∈ No )
8 onno ⊢ ( 𝐵 ∈ Ons → 𝐵 ∈ No )
9 8 adantl ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐵 ∈ No )
10 9 adantr ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → 𝐵 ∈ No )
11 7 10 mulscld ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑦 ·s 𝐵 ) ∈ No )
12 onno ⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )
13 12 adantr ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐴 ∈ No )
14 13 adantr ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → 𝐴 ∈ No )
15 leftno ⊢ ( 𝑧 ∈ ( L ‘ 𝐵 ) → 𝑧 ∈ No )
16 15 adantl ⊢ ( ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) → 𝑧 ∈ No )
17 16 adantl ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → 𝑧 ∈ No )
18 14 17 mulscld ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝐴 ·s 𝑧 ) ∈ No )
19 11 18 addscld ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) ∈ No )
20 7 17 mulscld ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑦 ·s 𝑧 ) ∈ No )
21 19 20 subscld ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ∈ No )
22 eleq1 ⊢ ( 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) → ( 𝑥 ∈ No ↔ ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) ∈ No ) )
23 21 22 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ ( 𝑦 ∈ ( L ‘ 𝐴 ) ∧ 𝑧 ∈ ( L ‘ 𝐵 ) ) ) → ( 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) → 𝑥 ∈ No ) )
24 23 rexlimdvva ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) → 𝑥 ∈ No ) )
25 24 abssdv ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) ∃ 𝑧 ∈ ( L ‘ 𝐵 ) 𝑥 = ( ( ( 𝑦 ·s 𝐵 ) +s ( 𝐴 ·s 𝑧 ) ) -s ( 𝑦 ·s 𝑧 ) ) } ⊆ No )
26 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
27 1 elpw ⊢ ( ( L ‘ 𝐴 ) ∈ 𝒫 No ↔ ( L ‘ 𝐴 ) ⊆ No )
28 26 27 mpbir ⊢ ( L ‘ 𝐴 ) ∈ 𝒫 No
29 nulsgts ⊢ ( ( L ‘ 𝐴 ) ∈ 𝒫 No → ( L ‘ 𝐴 ) <<s ∅ )
30 28 29 mp1i ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( L ‘ 𝐴 ) <<s ∅ )
31 leftssno ⊢ ( L ‘ 𝐵 ) ⊆ No
32 2 elpw ⊢ ( ( L ‘ 𝐵 ) ∈ 𝒫 No ↔ ( L ‘ 𝐵 ) ⊆ No )
33 31 32 mpbir ⊢ ( L ‘ 𝐵 ) ∈ 𝒫 No
34 nulsgts ⊢ ( ( L ‘ 𝐵 ) ∈ 𝒫 No → ( L ‘ 𝐵 ) <<s ∅ )
35 33 34 mp1i ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( L ‘ 𝐵 ) <<s ∅ )
36 oncutleft ⊢ ( 𝐴 ∈ Ons → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
37 36 adantr ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
38 oncutleft ⊢ ( 𝐵 ∈ Ons → 𝐵 = ( ( L ‘ 𝐵 ) |s ∅ ) )
39 38 adantl ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐵 = ( ( L ‘ 𝐵 ) |s ∅ ) )
40 30 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 25 56 elons2d ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 ·s 𝐵 ) ∈ Ons )