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 leftssno 
 |-  ( _Left ` A ) C_ No
8 7 sseli 
 |-  ( y e. ( _Left ` A ) -> y e. No )
9 8 adantl 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` A ) ) -> y e. No )
10 onsno 
 |-  ( B e. On_s -> B e. No )
11 10 ad2antlr 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` A ) ) -> B e. No )
12 9 11 addscld 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` A ) ) -> ( y +s B ) e. No )
13 eleq1 
 |-  ( x = ( y +s B ) -> ( x e. No <-> ( y +s B ) e. No ) )
14 12 13 syl5ibrcom 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` A ) ) -> ( x = ( y +s B ) -> x e. No ) )
15 14 rexlimdva 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( E. y e. ( _Left ` A ) x = ( y +s B ) -> x e. No ) )
16 15 abssdv 
 |-  ( ( A e. On_s /\ B e. On_s ) -> { x | E. y e. ( _Left ` A ) x = ( y +s B ) } C_ No )
17 onsno 
 |-  ( A e. On_s -> A e. No )
18 17 ad2antrr 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` B ) ) -> A e. No )
19 leftssno 
 |-  ( _Left ` B ) C_ No
20 19 sseli 
 |-  ( y e. ( _Left ` B ) -> y e. No )
21 20 adantl 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` B ) ) -> y e. No )
22 18 21 addscld 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` B ) ) -> ( A +s y ) e. No )
23 eleq1 
 |-  ( x = ( A +s y ) -> ( x e. No <-> ( A +s y ) e. No ) )
24 22 23 syl5ibrcom 
 |-  ( ( ( A e. On_s /\ B e. On_s ) /\ y e. ( _Left ` B ) ) -> ( x = ( A +s y ) -> x e. No ) )
25 24 rexlimdva 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( E. y e. ( _Left ` B ) x = ( A +s y ) -> x e. No ) )
26 25 abssdv 
 |-  ( ( A e. On_s /\ B e. On_s ) -> { x | E. y e. ( _Left ` B ) x = ( A +s y ) } C_ No )
27 16 26 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 )
28 1 elpw 
 |-  ( ( _Left ` A ) e. ~P No <-> ( _Left ` A ) C_ No )
29 7 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 3 elpw 
 |-  ( ( _Left ` B ) e. ~P No <-> ( _Left ` B ) C_ No )
33 19 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 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 27 49 elons2d 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( A +s B ) e. On_s )