Metamath Proof Explorer

Theorem addsunif

Description: Uniformity theorem for surreal addition. This theorem states that we can use any cuts that define A and B in the definition of surreal addition. Theorem 3.2 of Gonshor p. 15. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsunif.1 
|- ( ph -> L <
addsunif.2 
|- ( ph -> M <
addsunif.3 
|- ( ph -> A = ( L |s R ) )
addsunif.4 
|- ( ph -> B = ( M |s S ) )
Assertion addsunif 
|- ( ph -> ( A +s B ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) )

Proof

Step Hyp Ref Expression
1 addsunif.1 
 |-  ( ph -> L <
2 addsunif.2 
 |-  ( ph -> M <
3 addsunif.3 
 |-  ( ph -> A = ( L |s R ) )
4 addsunif.4 
 |-  ( ph -> B = ( M |s S ) )
5 1 2 3 4 addsuniflem 
 |-  ( ph -> ( A +s B ) = ( ( { a | E. b e. L a = ( b +s B ) } u. { c | E. d e. M c = ( A +s d ) } ) |s ( { e | E. f e. R e = ( f +s B ) } u. { g | E. h e. S g = ( A +s h ) } ) ) )
6 oveq1 
 |-  ( l = b -> ( l +s B ) = ( b +s B ) )
7 6 eqeq2d 
 |-  ( l = b -> ( y = ( l +s B ) <-> y = ( b +s B ) ) )
8 7 cbvrexvw 
 |-  ( E. l e. L y = ( l +s B ) <-> E. b e. L y = ( b +s B ) )
9 eqeq1 
 |-  ( y = a -> ( y = ( b +s B ) <-> a = ( b +s B ) ) )
10 9 rexbidv 
 |-  ( y = a -> ( E. b e. L y = ( b +s B ) <-> E. b e. L a = ( b +s B ) ) )
11 8 10 bitrid 
 |-  ( y = a -> ( E. l e. L y = ( l +s B ) <-> E. b e. L a = ( b +s B ) ) )
12 11 cbvabv 
 |-  { y | E. l e. L y = ( l +s B ) } = { a | E. b e. L a = ( b +s B ) }
13 oveq2 
 |-  ( m = d -> ( A +s m ) = ( A +s d ) )
14 13 eqeq2d 
 |-  ( m = d -> ( z = ( A +s m ) <-> z = ( A +s d ) ) )
15 14 cbvrexvw 
 |-  ( E. m e. M z = ( A +s m ) <-> E. d e. M z = ( A +s d ) )
16 eqeq1 
 |-  ( z = c -> ( z = ( A +s d ) <-> c = ( A +s d ) ) )
17 16 rexbidv 
 |-  ( z = c -> ( E. d e. M z = ( A +s d ) <-> E. d e. M c = ( A +s d ) ) )
18 15 17 bitrid 
 |-  ( z = c -> ( E. m e. M z = ( A +s m ) <-> E. d e. M c = ( A +s d ) ) )
19 18 cbvabv 
 |-  { z | E. m e. M z = ( A +s m ) } = { c | E. d e. M c = ( A +s d ) }
20 12 19 uneq12i 
 |-  ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) = ( { a | E. b e. L a = ( b +s B ) } u. { c | E. d e. M c = ( A +s d ) } )
21 oveq1 
 |-  ( r = f -> ( r +s B ) = ( f +s B ) )
22 21 eqeq2d 
 |-  ( r = f -> ( w = ( r +s B ) <-> w = ( f +s B ) ) )
23 22 cbvrexvw 
 |-  ( E. r e. R w = ( r +s B ) <-> E. f e. R w = ( f +s B ) )
24 eqeq1 
 |-  ( w = e -> ( w = ( f +s B ) <-> e = ( f +s B ) ) )
25 24 rexbidv 
 |-  ( w = e -> ( E. f e. R w = ( f +s B ) <-> E. f e. R e = ( f +s B ) ) )
26 23 25 bitrid 
 |-  ( w = e -> ( E. r e. R w = ( r +s B ) <-> E. f e. R e = ( f +s B ) ) )
27 26 cbvabv 
 |-  { w | E. r e. R w = ( r +s B ) } = { e | E. f e. R e = ( f +s B ) }
28 oveq2 
 |-  ( s = h -> ( A +s s ) = ( A +s h ) )
29 28 eqeq2d 
 |-  ( s = h -> ( t = ( A +s s ) <-> t = ( A +s h ) ) )
30 29 cbvrexvw 
 |-  ( E. s e. S t = ( A +s s ) <-> E. h e. S t = ( A +s h ) )
31 eqeq1 
 |-  ( t = g -> ( t = ( A +s h ) <-> g = ( A +s h ) ) )
32 31 rexbidv 
 |-  ( t = g -> ( E. h e. S t = ( A +s h ) <-> E. h e. S g = ( A +s h ) ) )
33 30 32 bitrid 
 |-  ( t = g -> ( E. s e. S t = ( A +s s ) <-> E. h e. S g = ( A +s h ) ) )
34 33 cbvabv 
 |-  { t | E. s e. S t = ( A +s s ) } = { g | E. h e. S g = ( A +s h ) }
35 27 34 uneq12i 
 |-  ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) = ( { e | E. f e. R e = ( f +s B ) } u. { g | E. h e. S g = ( A +s h ) } )
36 20 35 oveq12i 
 |-  ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) = ( ( { a | E. b e. L a = ( b +s B ) } u. { c | E. d e. M c = ( A +s d ) } ) |s ( { e | E. f e. R e = ( f +s B ) } u. { g | E. h e. S g = ( A +s h ) } ) )
37 5 36 eqtr4di 
 |-  ( ph -> ( A +s B ) = ( ( { y | E. l e. L y = ( l +s B ) } u. { z | E. m e. M z = ( A +s m ) } ) |s ( { w | E. r e. R w = ( r +s B ) } u. { t | E. s e. S t = ( A +s s ) } ) ) )