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 e. On_s /\ B e. On_s ) -> ( A x.s B ) e. On_s )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( _Left ` A ) e. _V
2 fvex 
 |-  ( _Left ` B ) e. _V
3 1 2 ab2rexex 
 |-  { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } e. _V
4 3 a1i 
 |-  ( ( A e. On_s /\ B e. On_s ) -> { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } e. _V )
5 leftssno 
 |-  ( _Left ` A ) C_ No
6 5 sseli 
 |-  ( y e. ( _Left ` A ) -> y e. No )
7 6 adantr 
 |-  ( ( y e. ( _Left ` A ) /\ z e. ( _Left ` B ) ) -> y e. No )
8 7 adantl 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ ( y e. ( _Left ` A ) /\ z e. ( _Left ` B ) ) ) -> y e. No )
9 onsno 
 |-  ( B e. On_s -> B e. No )
10 9 adantl 
 |-  ( ( A e. On_s /\ B e. On_s ) -> B e. No )
11 10 adantr 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ ( y e. ( _Left ` A ) /\ z e. ( _Left ` B ) ) ) -> B e. No )
12 8 11 mulscld 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ ( y e. ( _Left ` A ) /\ z e. ( _Left ` B ) ) ) -> ( y x.s B ) e. No )
13 onsno 
 |-  ( A e. On_s -> A e. No )
14 13 adantr 
 |-  ( ( A e. On_s /\ B e. On_s ) -> A e. No )
15 14 adantr 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ ( y e. ( _Left ` A ) /\ z e. ( _Left ` B ) ) ) -> A e. No )
16 leftssno 
 |-  ( _Left ` B ) C_ No
17 16 sseli 
 |-  ( z e. ( _Left ` B ) -> z e. No )
18 17 adantl 
 |-  ( ( y e. ( _Left ` A ) /\ z e. ( _Left ` B ) ) -> z e. No )
19 18 adantl 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ ( y e. ( _Left ` A ) /\ z e. ( _Left ` B ) ) ) -> z e. No )
20 15 19 mulscld 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ ( y e. ( _Left ` A ) /\ z e. ( _Left ` B ) ) ) -> ( A x.s z ) e. No )
21 12 20 addscld 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ ( y e. ( _Left ` A ) /\ z e. ( _Left ` B ) ) ) -> ( ( y x.s B ) +s ( A x.s z ) ) e. No )
22 8 19 mulscld 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ ( y e. ( _Left ` A ) /\ z e. ( _Left ` B ) ) ) -> ( y x.s z ) e. No )
23 21 22 subscld 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ ( y e. ( _Left ` A ) /\ z e. ( _Left ` B ) ) ) -> ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) e. No )
24 eleq1 
 |-  ( x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) -> ( x e. No <-> ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) e. No ) )
25 23 24 syl5ibrcom 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ ( y e. ( _Left ` A ) /\ z e. ( _Left ` B ) ) ) -> ( x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) -> x e. No ) )
26 25 rexlimdvva 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) -> x e. No ) )
27 26 abssdv 
 |-  ( ( A e. On_s /\ B e. On_s ) -> { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } C_ No )
28 1 elpw 
 |-  ( ( _Left ` A ) e. ~P No <-> ( _Left ` A ) C_ No )
29 5 28 mpbir 
 |-  ( _Left ` A ) e. ~P No
30 nulssgt 
 |-  ( ( _Left ` A ) e. ~P No -> ( _Left ` A ) <
31 29 30 mp1i 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( _Left ` A ) <
32 2 elpw 
 |-  ( ( _Left ` B ) e. ~P No <-> ( _Left ` B ) C_ No )
33 16 32 mpbir 
 |-  ( _Left ` B ) e. ~P No
34 nulssgt 
 |-  ( ( _Left ` B ) e. ~P No -> ( _Left ` B ) <
35 33 34 mp1i 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( _Left ` B ) <
36 onscutleft 
 |-  ( A e. On_s -> A = ( ( _Left ` A ) |s (/) ) )
37 36 adantr 
 |-  ( ( A e. On_s /\ B e. On_s ) -> A = ( ( _Left ` A ) |s (/) ) )
38 onscutleft 
 |-  ( B e. On_s -> B = ( ( _Left ` B ) |s (/) ) )
39 38 adantl 
 |-  ( ( A e. On_s /\ B e. On_s ) -> B = ( ( _Left ` B ) |s (/) ) )
40 31 35 37 39 mulsunif 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( A x.s B ) = ( ( { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } u. { x | E. y e. (/) E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } ) |s ( { x | E. y e. ( _Left ` A ) E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } u. { x | E. y e. (/) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } ) ) )
41 rex0 
 |-  -. E. y e. (/) E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) )
42 41 abf 
 |-  { x | E. y e. (/) E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } = (/)
43 42 uneq2i 
 |-  ( { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } u. { x | E. y e. (/) E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } ) = ( { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } u. (/) )
44 un0 
 |-  ( { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } u. (/) ) = { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) }
45 43 44 eqtri 
 |-  ( { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } u. { x | E. y e. (/) E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } ) = { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) }
46 rex0 
 |-  -. E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) )
47 46 a1i 
 |-  ( y e. ( _Left ` A ) -> -. E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) )
48 47 nrex 
 |-  -. E. y e. ( _Left ` A ) E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) )
49 48 abf 
 |-  { x | E. y e. ( _Left ` A ) E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } = (/)
50 rex0 
 |-  -. E. y e. (/) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) )
51 50 abf 
 |-  { x | E. y e. (/) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } = (/)
52 49 51 uneq12i 
 |-  ( { x | E. y e. ( _Left ` A ) E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } u. { x | E. y e. (/) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } ) = ( (/) u. (/) )
53 un0 
 |-  ( (/) u. (/) ) = (/)
54 52 53 eqtri 
 |-  ( { x | E. y e. ( _Left ` A ) E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } u. { x | E. y e. (/) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } ) = (/)
55 45 54 oveq12i 
 |-  ( ( { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } u. { x | E. y e. (/) E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } ) |s ( { x | E. y e. ( _Left ` A ) E. z e. (/) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } u. { x | E. y e. (/) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } ) ) = ( { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } |s (/) )
56 40 55 eqtrdi 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( A x.s B ) = ( { x | E. y e. ( _Left ` A ) E. z e. ( _Left ` B ) x = ( ( ( y x.s B ) +s ( A x.s z ) ) -s ( y x.s z ) ) } |s (/) ) )
57 4 27 56 elons2d 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( A x.s B ) e. On_s )