Metamath Proof Explorer

Theorem n0addscl

Description: The non-negative surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( n = 0s -> ( A +s n ) = ( A +s 0s ) )
2 1 eleq1d 
 |-  ( n = 0s -> ( ( A +s n ) e. NN0_s <-> ( A +s 0s ) e. NN0_s ) )
3 2 imbi2d 
 |-  ( n = 0s -> ( ( A e. NN0_s -> ( A +s n ) e. NN0_s ) <-> ( A e. NN0_s -> ( A +s 0s ) e. NN0_s ) ) )
4 oveq2 
 |-  ( n = m -> ( A +s n ) = ( A +s m ) )
5 4 eleq1d 
 |-  ( n = m -> ( ( A +s n ) e. NN0_s <-> ( A +s m ) e. NN0_s ) )
6 5 imbi2d 
 |-  ( n = m -> ( ( A e. NN0_s -> ( A +s n ) e. NN0_s ) <-> ( A e. NN0_s -> ( A +s m ) e. NN0_s ) ) )
7 oveq2 
 |-  ( n = ( m +s 1s ) -> ( A +s n ) = ( A +s ( m +s 1s ) ) )
8 7 eleq1d 
 |-  ( n = ( m +s 1s ) -> ( ( A +s n ) e. NN0_s <-> ( A +s ( m +s 1s ) ) e. NN0_s ) )
9 8 imbi2d 
 |-  ( n = ( m +s 1s ) -> ( ( A e. NN0_s -> ( A +s n ) e. NN0_s ) <-> ( A e. NN0_s -> ( A +s ( m +s 1s ) ) e. NN0_s ) ) )
10 oveq2 
 |-  ( n = B -> ( A +s n ) = ( A +s B ) )
11 10 eleq1d 
 |-  ( n = B -> ( ( A +s n ) e. NN0_s <-> ( A +s B ) e. NN0_s ) )
12 11 imbi2d 
 |-  ( n = B -> ( ( A e. NN0_s -> ( A +s n ) e. NN0_s ) <-> ( A e. NN0_s -> ( A +s B ) e. NN0_s ) ) )
13 n0sno 
 |-  ( A e. NN0_s -> A e. No )
14 13 addsridd 
 |-  ( A e. NN0_s -> ( A +s 0s ) = A )
15 id 
 |-  ( A e. NN0_s -> A e. NN0_s )
16 14 15 eqeltrd 
 |-  ( A e. NN0_s -> ( A +s 0s ) e. NN0_s )
17 13 adantr 
 |-  ( ( A e. NN0_s /\ m e. NN0_s ) -> A e. No )
18 17 adantr 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A +s m ) e. NN0_s ) -> A e. No )
19 n0sno 
 |-  ( m e. NN0_s -> m e. No )
20 19 adantl 
 |-  ( ( A e. NN0_s /\ m e. NN0_s ) -> m e. No )
21 20 adantr 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A +s m ) e. NN0_s ) -> m e. No )
22 1sno 
 |-  1s e. No
23 22 a1i 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A +s m ) e. NN0_s ) -> 1s e. No )
24 18 21 23 addsassd 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A +s m ) e. NN0_s ) -> ( ( A +s m ) +s 1s ) = ( A +s ( m +s 1s ) ) )
25 peano2n0s 
 |-  ( ( A +s m ) e. NN0_s -> ( ( A +s m ) +s 1s ) e. NN0_s )
26 25 adantl 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A +s m ) e. NN0_s ) -> ( ( A +s m ) +s 1s ) e. NN0_s )
27 24 26 eqeltrrd 
 |-  ( ( ( A e. NN0_s /\ m e. NN0_s ) /\ ( A +s m ) e. NN0_s ) -> ( A +s ( m +s 1s ) ) e. NN0_s )
28 27 ex 
 |-  ( ( A e. NN0_s /\ m e. NN0_s ) -> ( ( A +s m ) e. NN0_s -> ( A +s ( m +s 1s ) ) e. NN0_s ) )
29 28 expcom 
 |-  ( m e. NN0_s -> ( A e. NN0_s -> ( ( A +s m ) e. NN0_s -> ( A +s ( m +s 1s ) ) e. NN0_s ) ) )
30 29 a2d 
 |-  ( m e. NN0_s -> ( ( A e. NN0_s -> ( A +s m ) e. NN0_s ) -> ( A e. NN0_s -> ( A +s ( m +s 1s ) ) e. NN0_s ) ) )
31 3 6 9 12 16 30 n0sind 
 |-  ( B e. NN0_s -> ( A e. NN0_s -> ( A +s B ) e. NN0_s ) )
32 31 impcom 
 |-  ( ( A e. NN0_s /\ B e. NN0_s ) -> ( A +s B ) e. NN0_s )