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 ⊢φ→L≪sR
addsunif.2 ⊢φ→M≪sS
addsunif.3 ⊢φ→A=L|sR
addsunif.4 ⊢φ→B=M|sS
Assertion addsunif Could not format assertion : No typesetting found for |- ( 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 ) } ) ) ) with typecode |-

Proof

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