Metamath Proof Explorer

Theorem onaddscl

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

Ref Expression
Assertion onaddscl 
|- ( ( A e. On_s /\ B e. On_s ) -> ( A +s B ) e. On_s )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( _Left ` A ) e. _V
2 1 abrexex 
 |-  { x | E. y e. ( _Left ` A ) x = ( y +s B ) } e. _V
3 fvex 
 |-  ( _Left ` B ) e. _V
4 3 abrexex 
 |-  { x | E. y e. ( _Left ` B ) x = ( A +s y ) } e. _V
5 2 4 unex 
 |-  ( { x | E. y e. ( _Left ` A ) x = ( y +s B ) } u. { x | E. y e. ( _Left ` B ) x = ( A +s y ) } ) e. _V
6 5 a1i 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( { x | E. y e. ( _Left ` A ) x = ( y +s B ) } u. { x | E. y e. ( _Left ` B ) x = ( A +s y ) } ) e. _V )
7 leftno 
 |-  ( y e. ( _Left ` A ) -> y e. No )
8 7 adantl 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` A ) ) -> y e. No )
9 onno 
 |-  ( B e. On_s -> B e. No )
10 9 ad2antlr 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` A ) ) -> B e. No )
11 8 10 addscld 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` A ) ) -> ( y +s B ) e. No )
12 eleq1 
 |-  ( x = ( y +s B ) -> ( x e. No <-> ( y +s B ) e. No ) )
13 11 12 syl5ibrcom 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` A ) ) -> ( x = ( y +s B ) -> x e. No ) )
14 13 rexlimdva 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( E. y e. ( _Left ` A ) x = ( y +s B ) -> x e. No ) )
15 14 abssdv 
 |-  ( ( A e. On_s /\ B e. On_s ) -> { x | E. y e. ( _Left ` A ) x = ( y +s B ) } C_ No )
16 onno 
 |-  ( A e. On_s -> A e. No )
17 16 ad2antrr 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` B ) ) -> A e. No )
18 leftno 
 |-  ( y e. ( _Left ` B ) -> y e. No )
19 18 adantl 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` B ) ) -> y e. No )
20 17 19 addscld 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` B ) ) -> ( A +s y ) e. No )
21 eleq1 
 |-  ( x = ( A +s y ) -> ( x e. No <-> ( A +s y ) e. No ) )
22 20 21 syl5ibrcom 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` B ) ) -> ( x = ( A +s y ) -> x e. No ) )
23 22 rexlimdva 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( E. y e. ( _Left ` B ) x = ( A +s y ) -> x e. No ) )
24 23 abssdv 
 |-  ( ( A e. On_s /\ B e. On_s ) -> { x | E. y e. ( _Left ` B ) x = ( A +s y ) } C_ No )
25 15 24 unssd 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( { x | E. y e. ( _Left ` A ) x = ( y +s B ) } u. { x | E. y e. ( _Left ` B ) x = ( A +s y ) } ) C_ No )
26 leftssno 
 |-  ( _Left ` A ) C_ No
27 1 elpw 
 |-  ( ( _Left ` A ) e. ~P No <-> ( _Left ` A ) C_ No )
28 26 27 mpbir 
 |-  ( _Left ` A ) e. ~P No
29 nulsgts 
 |-  ( ( _Left ` A ) e. ~P No -> ( _Left ` A ) <
30 28 29 mp1i 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( _Left ` A ) <
31 leftssno 
 |-  ( _Left ` B ) C_ No
32 3 elpw 
 |-  ( ( _Left ` B ) e. ~P No <-> ( _Left ` B ) C_ No )
33 31 32 mpbir 
 |-  ( _Left ` B ) e. ~P No
34 nulsgts 
 |-  ( ( _Left ` B ) e. ~P No -> ( _Left ` B ) <
35 33 34 mp1i 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( _Left ` B ) <
36 oncutleft 
 |-  ( A e. On_s -> A = ( ( _Left ` A ) |s (/) ) )
37 36 adantr 
 |-  ( ( A e. On_s /\ B e. On_s ) -> A = ( ( _Left ` A ) |s (/) ) )
38 oncutleft 
 |-  ( B e. On_s -> B = ( ( _Left ` B ) |s (/) ) )
39 38 adantl 
 |-  ( ( A e. On_s /\ B e. On_s ) -> B = ( ( _Left ` B ) |s (/) ) )
40 30 35 37 39 addsunif 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( A +s B ) = ( ( { x | E. y e. ( _Left ` A ) x = ( y +s B ) } u. { x | E. y e. ( _Left ` B ) x = ( A +s y ) } ) |s ( { x | E. y e. (/) x = ( y +s B ) } u. { x | E. y e. (/) x = ( A +s y ) } ) ) )
41 rex0 
 |-  -. E. y e. (/) x = ( y +s B )
42 41 abf 
 |-  { x | E. y e. (/) x = ( y +s B ) } = (/)
43 rex0 
 |-  -. E. y e. (/) x = ( A +s y )
44 43 abf 
 |-  { x | E. y e. (/) x = ( A +s y ) } = (/)
45 42 44 uneq12i 
 |-  ( { x | E. y e. (/) x = ( y +s B ) } u. { x | E. y e. (/) x = ( A +s y ) } ) = ( (/) u. (/) )
46 un0 
 |-  ( (/) u. (/) ) = (/)
47 45 46 eqtri 
 |-  ( { x | E. y e. (/) x = ( y +s B ) } u. { x | E. y e. (/) x = ( A +s y ) } ) = (/)
48 47 oveq2i 
 |-  ( ( { x | E. y e. ( _Left ` A ) x = ( y +s B ) } u. { x | E. y e. ( _Left ` B ) x = ( A +s y ) } ) |s ( { x | E. y e. (/) x = ( y +s B ) } u. { x | E. y e. (/) x = ( A +s y ) } ) ) = ( ( { x | E. y e. ( _Left ` A ) x = ( y +s B ) } u. { x | E. y e. ( _Left ` B ) x = ( A +s y ) } ) |s (/) )
49 40 48 eqtrdi 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( A +s B ) = ( ( { x | E. y e. ( _Left ` A ) x = ( y +s B ) } u. { x | E. y e. ( _Left ` B ) x = ( A +s y ) } ) |s (/) ) )
50 6 25 49 elons2d 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( A +s B ) e. On_s )