Theorem addscllem1

Description: Lemma for addscl (future) Alternate expression for surreal addition. (Contributed by Scott Fenton, 23-Aug-2024)

	Ref	Expression
Assertion	addscllem1	|- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( ( +s " ( ( _L ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _L ` B ) ) ) ) |s ( ( +s " ( ( _R ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _R ` B ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		addsov	|- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { x | E. l e. ( _L ` A ) x = ( l +s B ) } u. { y | E. l e. ( _L ` B ) y = ( A +s l ) } ) |s ( { x | E. r e. ( _R ` A ) x = ( r +s B ) } u. { y | E. r e. ( _R ` B ) y = ( A +s r ) } ) ) )
2		addsfn	|- +s Fn ( No X. No )
3		leftssno	|- ( A e. No -> ( _L ` A ) C_ No )
4		snssi	|- ( B e. No -> { B } C_ No )
5		xpss12	|- ( ( ( _L ` A ) C_ No /\ { B } C_ No ) -> ( ( _L ` A ) X. { B } ) C_ ( No X. No ) )
6	3 4 5	syl2an	|- ( ( A e. No /\ B e. No ) -> ( ( _L ` A ) X. { B } ) C_ ( No X. No ) )
7		ovelimab	|- ( ( +s Fn ( No X. No ) /\ ( ( _L ` A ) X. { B } ) C_ ( No X. No ) ) -> ( x e. ( +s " ( ( _L ` A ) X. { B } ) ) <-> E. l e. ( _L ` A ) E. r e. { B } x = ( l +s r ) ) )
8	2 6 7	sylancr	|- ( ( A e. No /\ B e. No ) -> ( x e. ( +s " ( ( _L ` A ) X. { B } ) ) <-> E. l e. ( _L ` A ) E. r e. { B } x = ( l +s r ) ) )
9		oveq2	|- ( r = B -> ( l +s r ) = ( l +s B ) )
10	9	eqeq2d	|- ( r = B -> ( x = ( l +s r ) <-> x = ( l +s B ) ) )
11	10	rexsng	|- ( B e. No -> ( E. r e. { B } x = ( l +s r ) <-> x = ( l +s B ) ) )
12	11	adantl	|- ( ( A e. No /\ B e. No ) -> ( E. r e. { B } x = ( l +s r ) <-> x = ( l +s B ) ) )
13	12	rexbidv	|- ( ( A e. No /\ B e. No ) -> ( E. l e. ( _L ` A ) E. r e. { B } x = ( l +s r ) <-> E. l e. ( _L ` A ) x = ( l +s B ) ) )
14	8 13	bitrd	|- ( ( A e. No /\ B e. No ) -> ( x e. ( +s " ( ( _L ` A ) X. { B } ) ) <-> E. l e. ( _L ` A ) x = ( l +s B ) ) )
15	14	abbi2dv	|- ( ( A e. No /\ B e. No ) -> ( +s " ( ( _L ` A ) X. { B } ) ) = { x | E. l e. ( _L ` A ) x = ( l +s B ) } )
16		snssi	|- ( A e. No -> { A } C_ No )
17		leftssno	|- ( B e. No -> ( _L ` B ) C_ No )
18		xpss12	|- ( ( { A } C_ No /\ ( _L ` B ) C_ No ) -> ( { A } X. ( _L ` B ) ) C_ ( No X. No ) )
19	16 17 18	syl2an	|- ( ( A e. No /\ B e. No ) -> ( { A } X. ( _L ` B ) ) C_ ( No X. No ) )
20		ovelimab	|- ( ( +s Fn ( No X. No ) /\ ( { A } X. ( _L ` B ) ) C_ ( No X. No ) ) -> ( y e. ( +s " ( { A } X. ( _L ` B ) ) ) <-> E. r e. { A } E. l e. ( _L ` B ) y = ( r +s l ) ) )
21	2 19 20	sylancr	|- ( ( A e. No /\ B e. No ) -> ( y e. ( +s " ( { A } X. ( _L ` B ) ) ) <-> E. r e. { A } E. l e. ( _L ` B ) y = ( r +s l ) ) )
22		oveq1	|- ( r = A -> ( r +s l ) = ( A +s l ) )
23	22	eqeq2d	|- ( r = A -> ( y = ( r +s l ) <-> y = ( A +s l ) ) )
24	23	rexbidv	|- ( r = A -> ( E. l e. ( _L ` B ) y = ( r +s l ) <-> E. l e. ( _L ` B ) y = ( A +s l ) ) )
25	24	rexsng	|- ( A e. No -> ( E. r e. { A } E. l e. ( _L ` B ) y = ( r +s l ) <-> E. l e. ( _L ` B ) y = ( A +s l ) ) )
26	25	adantr	|- ( ( A e. No /\ B e. No ) -> ( E. r e. { A } E. l e. ( _L ` B ) y = ( r +s l ) <-> E. l e. ( _L ` B ) y = ( A +s l ) ) )
27	21 26	bitrd	|- ( ( A e. No /\ B e. No ) -> ( y e. ( +s " ( { A } X. ( _L ` B ) ) ) <-> E. l e. ( _L ` B ) y = ( A +s l ) ) )
28	27	abbi2dv	|- ( ( A e. No /\ B e. No ) -> ( +s " ( { A } X. ( _L ` B ) ) ) = { y | E. l e. ( _L ` B ) y = ( A +s l ) } )
29	15 28	uneq12d	|- ( ( A e. No /\ B e. No ) -> ( ( +s " ( ( _L ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _L ` B ) ) ) ) = ( { x | E. l e. ( _L ` A ) x = ( l +s B ) } u. { y | E. l e. ( _L ` B ) y = ( A +s l ) } ) )
30		rightssno	|- ( A e. No -> ( _R ` A ) C_ No )
31		xpss12	|- ( ( ( _R ` A ) C_ No /\ { B } C_ No ) -> ( ( _R ` A ) X. { B } ) C_ ( No X. No ) )
32	30 4 31	syl2an	|- ( ( A e. No /\ B e. No ) -> ( ( _R ` A ) X. { B } ) C_ ( No X. No ) )
33		ovelimab	|- ( ( +s Fn ( No X. No ) /\ ( ( _R ` A ) X. { B } ) C_ ( No X. No ) ) -> ( x e. ( +s " ( ( _R ` A ) X. { B } ) ) <-> E. r e. ( _R ` A ) E. l e. { B } x = ( r +s l ) ) )
34	2 32 33	sylancr	|- ( ( A e. No /\ B e. No ) -> ( x e. ( +s " ( ( _R ` A ) X. { B } ) ) <-> E. r e. ( _R ` A ) E. l e. { B } x = ( r +s l ) ) )
35		oveq2	|- ( l = B -> ( r +s l ) = ( r +s B ) )
36	35	eqeq2d	|- ( l = B -> ( x = ( r +s l ) <-> x = ( r +s B ) ) )
37	36	rexsng	|- ( B e. No -> ( E. l e. { B } x = ( r +s l ) <-> x = ( r +s B ) ) )
38	37	adantl	|- ( ( A e. No /\ B e. No ) -> ( E. l e. { B } x = ( r +s l ) <-> x = ( r +s B ) ) )
39	38	rexbidv	|- ( ( A e. No /\ B e. No ) -> ( E. r e. ( _R ` A ) E. l e. { B } x = ( r +s l ) <-> E. r e. ( _R ` A ) x = ( r +s B ) ) )
40	34 39	bitrd	|- ( ( A e. No /\ B e. No ) -> ( x e. ( +s " ( ( _R ` A ) X. { B } ) ) <-> E. r e. ( _R ` A ) x = ( r +s B ) ) )
41	40	abbi2dv	|- ( ( A e. No /\ B e. No ) -> ( +s " ( ( _R ` A ) X. { B } ) ) = { x | E. r e. ( _R ` A ) x = ( r +s B ) } )
42		rightssno	|- ( B e. No -> ( _R ` B ) C_ No )
43		xpss12	|- ( ( { A } C_ No /\ ( _R ` B ) C_ No ) -> ( { A } X. ( _R ` B ) ) C_ ( No X. No ) )
44	16 42 43	syl2an	|- ( ( A e. No /\ B e. No ) -> ( { A } X. ( _R ` B ) ) C_ ( No X. No ) )
45		ovelimab	|- ( ( +s Fn ( No X. No ) /\ ( { A } X. ( _R ` B ) ) C_ ( No X. No ) ) -> ( y e. ( +s " ( { A } X. ( _R ` B ) ) ) <-> E. l e. { A } E. r e. ( _R ` B ) y = ( l +s r ) ) )
46	2 44 45	sylancr	|- ( ( A e. No /\ B e. No ) -> ( y e. ( +s " ( { A } X. ( _R ` B ) ) ) <-> E. l e. { A } E. r e. ( _R ` B ) y = ( l +s r ) ) )
47		oveq1	|- ( l = A -> ( l +s r ) = ( A +s r ) )
48	47	eqeq2d	|- ( l = A -> ( y = ( l +s r ) <-> y = ( A +s r ) ) )
49	48	rexbidv	|- ( l = A -> ( E. r e. ( _R ` B ) y = ( l +s r ) <-> E. r e. ( _R ` B ) y = ( A +s r ) ) )
50	49	rexsng	|- ( A e. No -> ( E. l e. { A } E. r e. ( _R ` B ) y = ( l +s r ) <-> E. r e. ( _R ` B ) y = ( A +s r ) ) )
51	50	adantr	|- ( ( A e. No /\ B e. No ) -> ( E. l e. { A } E. r e. ( _R ` B ) y = ( l +s r ) <-> E. r e. ( _R ` B ) y = ( A +s r ) ) )
52	46 51	bitrd	|- ( ( A e. No /\ B e. No ) -> ( y e. ( +s " ( { A } X. ( _R ` B ) ) ) <-> E. r e. ( _R ` B ) y = ( A +s r ) ) )
53	52	abbi2dv	|- ( ( A e. No /\ B e. No ) -> ( +s " ( { A } X. ( _R ` B ) ) ) = { y | E. r e. ( _R ` B ) y = ( A +s r ) } )
54	41 53	uneq12d	|- ( ( A e. No /\ B e. No ) -> ( ( +s " ( ( _R ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _R ` B ) ) ) ) = ( { x | E. r e. ( _R ` A ) x = ( r +s B ) } u. { y | E. r e. ( _R ` B ) y = ( A +s r ) } ) )
55	29 54	oveq12d	|- ( ( A e. No /\ B e. No ) -> ( ( ( +s " ( ( _L ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _L ` B ) ) ) ) |s ( ( +s " ( ( _R ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _R ` B ) ) ) ) ) = ( ( { x | E. l e. ( _L ` A ) x = ( l +s B ) } u. { y | E. l e. ( _L ` B ) y = ( A +s l ) } ) |s ( { x | E. r e. ( _R ` A ) x = ( r +s B ) } u. { y | E. r e. ( _R ` B ) y = ( A +s r ) } ) ) )
56	1 55	eqtr4d	|- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( ( +s " ( ( _L ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _L ` B ) ) ) ) |s ( ( +s " ( ( _R ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _R ` B ) ) ) ) ) )