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	$$⊢\phi \to L{\ll }_{s}R$$
	addsunif.2	$$⊢\phi \to M{\ll }_{s}S$$
	addsunif.3	$$⊢\phi \to A=L{|}_{s}R$$
	addsunif.4	$$⊢\phi \to B=M{|}_{s}S$$
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	$$⊢\phi \to L{\ll }_{s}R$$
2		addsunif.2	$$⊢\phi \to M{\ll }_{s}S$$
3		addsunif.3	$$⊢\phi \to A=L{|}_{s}R$$
4		addsunif.4	$$⊢\phi \to B=M{|}_{s}S$$
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 |-