Theorem addscut

Description: Demonstrate the cut properties of surreal addition. This gives us closure together with a pair of set-less-than relationships for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addscut.1	$$⊢\phi \to X\in \mathrm{No}$$
	addscut.2	$$⊢\phi \to Y\in \mathrm{No}$$
Assertion	addscut	Could not format assertion : No typesetting found for |- ( ph -> ( ( X +s Y ) e. No /\ ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <

Proof

Step	Hyp	Ref	Expression
1		addscut.1	$$⊢\phi \to X\in \mathrm{No}$$
2		addscut.2	$$⊢\phi \to Y\in \mathrm{No}$$
3	1 2	addscutlem	Could not format ( ph -> ( ( X +s Y ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) < ( ( X +s Y ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) <
4		biid	Could not format ( ( X +s Y ) e. No <-> ( X +s Y ) e. No ) : No typesetting found for |- ( ( X +s Y ) e. No <-> ( X +s Y ) e. No ) with typecode |-
5		oveq1	Could not format ( l = b -> ( l +s Y ) = ( b +s Y ) ) : No typesetting found for |- ( l = b -> ( l +s Y ) = ( b +s Y ) ) with typecode |-
6	5	eqeq2d	Could not format ( l = b -> ( p = ( l +s Y ) <-> p = ( b +s Y ) ) ) : No typesetting found for |- ( l = b -> ( p = ( l +s Y ) <-> p = ( b +s Y ) ) ) with typecode |-
7	6	cbvrexvw	Could not format ( E. l e. ( _Left ` X ) p = ( l +s Y ) <-> E. b e. ( _Left ` X ) p = ( b +s Y ) ) : No typesetting found for |- ( E. l e. ( _Left ` X ) p = ( l +s Y ) <-> E. b e. ( _Left ` X ) p = ( b +s Y ) ) with typecode |-
8		eqeq1	Could not format ( p = a -> ( p = ( b +s Y ) <-> a = ( b +s Y ) ) ) : No typesetting found for |- ( p = a -> ( p = ( b +s Y ) <-> a = ( b +s Y ) ) ) with typecode |-
9	8	rexbidv	Could not format ( p = a -> ( E. b e. ( _Left ` X ) p = ( b +s Y ) <-> E. b e. ( _Left ` X ) a = ( b +s Y ) ) ) : No typesetting found for |- ( p = a -> ( E. b e. ( _Left ` X ) p = ( b +s Y ) <-> E. b e. ( _Left ` X ) a = ( b +s Y ) ) ) with typecode |-
10	7 9	bitrid	Could not format ( p = a -> ( E. l e. ( _Left ` X ) p = ( l +s Y ) <-> E. b e. ( _Left ` X ) a = ( b +s Y ) ) ) : No typesetting found for |- ( p = a -> ( E. l e. ( _Left ` X ) p = ( l +s Y ) <-> E. b e. ( _Left ` X ) a = ( b +s Y ) ) ) with typecode |-
11	10	cbvabv	Could not format { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } = { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } : No typesetting found for |- { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } = { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } with typecode |-
12		oveq2	Could not format ( m = d -> ( X +s m ) = ( X +s d ) ) : No typesetting found for |- ( m = d -> ( X +s m ) = ( X +s d ) ) with typecode |-
13	12	eqeq2d	Could not format ( m = d -> ( q = ( X +s m ) <-> q = ( X +s d ) ) ) : No typesetting found for |- ( m = d -> ( q = ( X +s m ) <-> q = ( X +s d ) ) ) with typecode |-
14	13	cbvrexvw	Could not format ( E. m e. ( _Left ` Y ) q = ( X +s m ) <-> E. d e. ( _Left ` Y ) q = ( X +s d ) ) : No typesetting found for |- ( E. m e. ( _Left ` Y ) q = ( X +s m ) <-> E. d e. ( _Left ` Y ) q = ( X +s d ) ) with typecode |-
15		eqeq1	Could not format ( q = c -> ( q = ( X +s d ) <-> c = ( X +s d ) ) ) : No typesetting found for |- ( q = c -> ( q = ( X +s d ) <-> c = ( X +s d ) ) ) with typecode |-
16	15	rexbidv	Could not format ( q = c -> ( E. d e. ( _Left ` Y ) q = ( X +s d ) <-> E. d e. ( _Left ` Y ) c = ( X +s d ) ) ) : No typesetting found for |- ( q = c -> ( E. d e. ( _Left ` Y ) q = ( X +s d ) <-> E. d e. ( _Left ` Y ) c = ( X +s d ) ) ) with typecode |-
17	14 16	bitrid	Could not format ( q = c -> ( E. m e. ( _Left ` Y ) q = ( X +s m ) <-> E. d e. ( _Left ` Y ) c = ( X +s d ) ) ) : No typesetting found for |- ( q = c -> ( E. m e. ( _Left ` Y ) q = ( X +s m ) <-> E. d e. ( _Left ` Y ) c = ( X +s d ) ) ) with typecode |-
18	17	cbvabv	Could not format { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } = { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } : No typesetting found for |- { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } = { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } with typecode |-
19	11 18	uneq12i	Could not format ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) = ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) : No typesetting found for |- ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) = ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) with typecode |-
20	19	breq1i	Could not format ( ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) < ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) <
21		oveq1	Could not format ( r = f -> ( r +s Y ) = ( f +s Y ) ) : No typesetting found for |- ( r = f -> ( r +s Y ) = ( f +s Y ) ) with typecode |-
22	21	eqeq2d	Could not format ( r = f -> ( w = ( r +s Y ) <-> w = ( f +s Y ) ) ) : No typesetting found for |- ( r = f -> ( w = ( r +s Y ) <-> w = ( f +s Y ) ) ) with typecode |-
23	22	cbvrexvw	Could not format ( E. r e. ( _Right ` X ) w = ( r +s Y ) <-> E. f e. ( _Right ` X ) w = ( f +s Y ) ) : No typesetting found for |- ( E. r e. ( _Right ` X ) w = ( r +s Y ) <-> E. f e. ( _Right ` X ) w = ( f +s Y ) ) with typecode |-
24		eqeq1	Could not format ( w = e -> ( w = ( f +s Y ) <-> e = ( f +s Y ) ) ) : No typesetting found for |- ( w = e -> ( w = ( f +s Y ) <-> e = ( f +s Y ) ) ) with typecode |-
25	24	rexbidv	Could not format ( w = e -> ( E. f e. ( _Right ` X ) w = ( f +s Y ) <-> E. f e. ( _Right ` X ) e = ( f +s Y ) ) ) : No typesetting found for |- ( w = e -> ( E. f e. ( _Right ` X ) w = ( f +s Y ) <-> E. f e. ( _Right ` X ) e = ( f +s Y ) ) ) with typecode |-
26	23 25	bitrid	Could not format ( w = e -> ( E. r e. ( _Right ` X ) w = ( r +s Y ) <-> E. f e. ( _Right ` X ) e = ( f +s Y ) ) ) : No typesetting found for |- ( w = e -> ( E. r e. ( _Right ` X ) w = ( r +s Y ) <-> E. f e. ( _Right ` X ) e = ( f +s Y ) ) ) with typecode |-
27	26	cbvabv	Could not format { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } = { e | E. f e. ( _Right ` X ) e = ( f +s Y ) } : No typesetting found for |- { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } = { e | E. f e. ( _Right ` X ) e = ( f +s Y ) } with typecode |-
28		oveq2	Could not format ( s = h -> ( X +s s ) = ( X +s h ) ) : No typesetting found for |- ( s = h -> ( X +s s ) = ( X +s h ) ) with typecode |-
29	28	eqeq2d	Could not format ( s = h -> ( t = ( X +s s ) <-> t = ( X +s h ) ) ) : No typesetting found for |- ( s = h -> ( t = ( X +s s ) <-> t = ( X +s h ) ) ) with typecode |-
30	29	cbvrexvw	Could not format ( E. s e. ( _Right ` Y ) t = ( X +s s ) <-> E. h e. ( _Right ` Y ) t = ( X +s h ) ) : No typesetting found for |- ( E. s e. ( _Right ` Y ) t = ( X +s s ) <-> E. h e. ( _Right ` Y ) t = ( X +s h ) ) with typecode |-
31		eqeq1	Could not format ( t = g -> ( t = ( X +s h ) <-> g = ( X +s h ) ) ) : No typesetting found for |- ( t = g -> ( t = ( X +s h ) <-> g = ( X +s h ) ) ) with typecode |-
32	31	rexbidv	Could not format ( t = g -> ( E. h e. ( _Right ` Y ) t = ( X +s h ) <-> E. h e. ( _Right ` Y ) g = ( X +s h ) ) ) : No typesetting found for |- ( t = g -> ( E. h e. ( _Right ` Y ) t = ( X +s h ) <-> E. h e. ( _Right ` Y ) g = ( X +s h ) ) ) with typecode |-
33	30 32	bitrid	Could not format ( t = g -> ( E. s e. ( _Right ` Y ) t = ( X +s s ) <-> E. h e. ( _Right ` Y ) g = ( X +s h ) ) ) : No typesetting found for |- ( t = g -> ( E. s e. ( _Right ` Y ) t = ( X +s s ) <-> E. h e. ( _Right ` Y ) g = ( X +s h ) ) ) with typecode |-
34	33	cbvabv	Could not format { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } = { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } : No typesetting found for |- { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } = { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } with typecode |-
35	27 34	uneq12i	Could not format ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) = ( { e | E. f e. ( _Right ` X ) e = ( f +s Y ) } u. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } ) : No typesetting found for |- ( { w | E. r e. ( _Right ` X ) w = ( r +s Y ) } u. { t | E. s e. ( _Right ` Y ) t = ( X +s s ) } ) = ( { e | E. f e. ( _Right ` X ) e = ( f +s Y ) } u. { g | E. h e. ( _Right ` Y ) g = ( X +s h ) } ) with typecode |-
36	35	breq2i	Could not format ( { ( X +s Y ) } < { ( X +s Y ) } < { ( X +s Y ) } <
37	4 20 36	3anbi123i	Could not format ( ( ( X +s Y ) e. No /\ ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( ( X +s Y ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) < ( ( X +s Y ) e. No /\ ( { a | E. b e. ( _Left ` X ) a = ( b +s Y ) } u. { c | E. d e. ( _Left ` Y ) c = ( X +s d ) } ) <
38	3 37	sylibr	Could not format ( ph -> ( ( X +s Y ) e. No /\ ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( ( X +s Y ) e. No /\ ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <