Theorem addscllem1

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

	Ref	Expression
Assertion	addscllem1	Could not format assertion : No typesetting found for |- ( ( 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 ) ) ) ) ) ) with typecode |-

Proof

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