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		addsval	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	$$⊢L\left(A\right)\subseteq \mathrm{No}$$
4	3	a1i	$$⊢A\in \mathrm{No}\to L\left(A\right)\subseteq \mathrm{No}$$
5		snssi	$$⊢B\in \mathrm{No}\to \left\{B\right\}\subseteq \mathrm{No}$$
6		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}$$
7	4 5 6	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}$$
8		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 |-
9	2 7 8	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 |-
10		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 |-
11	10	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 |-
12	11	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 |-
13	12	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 |-
14	13	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 |-
15	9 14	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 |-
16	15	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 |-
17		snssi	$$⊢A\in \mathrm{No}\to \left\{A\right\}\subseteq \mathrm{No}$$
18		leftssno	$$⊢L\left(B\right)\subseteq \mathrm{No}$$
19	18	a1i	$$⊢B\in \mathrm{No}\to L\left(B\right)\subseteq \mathrm{No}$$
20		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}$$
21	17 19 20	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}$$
22		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 |-
23	2 21 22	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 |-
24		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 |-
25	24	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 |-
26	25	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 |-
27	26	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 |-
28	27	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 |-
29	23 28	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 |-
30	29	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 |-
31	16 30	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 |-
32		rightssno	$$⊢R\left(A\right)\subseteq \mathrm{No}$$
33	32	a1i	$$⊢A\in \mathrm{No}\to R\left(A\right)\subseteq \mathrm{No}$$
34		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}$$
35	33 5 34	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}$$
36		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 |-
37	2 35 36	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 |-
38		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 |-
39	38	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 |-
40	39	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 |-
41	40	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 |-
42	41	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 |-
43	37 42	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 |-
44	43	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 |-
45		rightssno	$$⊢R\left(B\right)\subseteq \mathrm{No}$$
46	45	a1i	$$⊢B\in \mathrm{No}\to R\left(B\right)\subseteq \mathrm{No}$$
47		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}$$
48	17 46 47	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}$$
49		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 |-
50	2 48 49	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 |-
51		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 |-
52	51	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 |-
53	52	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 |-
54	53	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 |-
55	54	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 |-
56	50 55	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 |-
57	56	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 |-
58	44 57	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 |-
59	31 58	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 |-
60	1 59	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 |-