Theorem negsproplem2

Description: Lemma for surreal negation. Show that the cut that defines negation is legitimate. (Contributed by Scott Fenton, 2-Feb-2025)

	Ref	Expression
Hypotheses	negsproplem.1	$$⊢\phi \to \forall x\in \mathrm{No}\forall y\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\right)$$
	negsproplem2.1	$$⊢\phi \to A\in \mathrm{No}$$
Assertion	negsproplem2	$$⊢\phi \to {+}_s\left[R\left(A\right)\right]{\ll }_s{+}_s\left[L\left(A\right)\right]$$

Proof

Step	Hyp	Ref	Expression
1		negsproplem.1	$$⊢\phi \to \forall x\in \mathrm{No}\forall y\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\right)$$
2		negsproplem2.1	$$⊢\phi \to A\in \mathrm{No}$$
3		negsfn	$$⊢{+}_{s}Fn\mathrm{No}$$
4		fnfun	$$⊢{+}_{s}Fn\mathrm{No}\to \mathrm{Fun}{+}_s$$
5	3 4	ax-mp	$$⊢\mathrm{Fun}{+}_s$$
6		fvex	$$⊢R\left(A\right)\in \mathrm{V}$$
7	6	funimaex	$$⊢\mathrm{Fun}{+}_s\to {+}_s\left[R\left(A\right)\right]\in \mathrm{V}$$
8	5 7	mp1i	$$⊢\phi \to {+}_s\left[R\left(A\right)\right]\in \mathrm{V}$$
9		fvex	$$⊢L\left(A\right)\in \mathrm{V}$$
10	9	funimaex	$$⊢\mathrm{Fun}{+}_s\to {+}_s\left[L\left(A\right)\right]\in \mathrm{V}$$
11	5 10	mp1i	$$⊢\phi \to {+}_s\left[L\left(A\right)\right]\in \mathrm{V}$$
12		rightssold	$$⊢R\left(A\right)\subseteq \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
13		imass2	$$⊢R\left(A\right)\subseteq \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\to {+}_s\left[R\left(A\right)\right]\subseteq {+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right]$$
14	12 13	ax-mp	$$⊢{+}_s\left[R\left(A\right)\right]\subseteq {+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right]$$
15	1	adantr	$$⊢\left(\phi \wedge a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right)\to \forall x\in \mathrm{No}\forall y\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\right)$$
16		oldssno	$$⊢\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\subseteq \mathrm{No}$$
17	16	sseli	$$⊢a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\to a\in \mathrm{No}$$
18	17	adantl	$$⊢\left(\phi \wedge a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right)\to a\in \mathrm{No}$$
19		0sno	$$⊢0_s\in \mathrm{No}$$
20	19	a1i	$$⊢\left(\phi \wedge a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right)\to 0_s\in \mathrm{No}$$
21		bday0s	$$⊢\mathrm{bday}\left(0_s\right)=\varnothing$$
22	21	uneq2i	$$⊢\mathrm{bday}\left(a\right)\cup \mathrm{bday}\left(0_s\right)=\mathrm{bday}\left(a\right)\cup \varnothing$$
23		un0	$$⊢\mathrm{bday}\left(a\right)\cup \varnothing =\mathrm{bday}\left(a\right)$$
24	22 23	eqtri	$$⊢\mathrm{bday}\left(a\right)\cup \mathrm{bday}\left(0_s\right)=\mathrm{bday}\left(a\right)$$
25		oldbdayim	$$⊢a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\to \mathrm{bday}\left(a\right)\in \mathrm{bday}\left(A\right)$$
26	25	adantl	$$⊢\left(\phi \wedge a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right)\to \mathrm{bday}\left(a\right)\in \mathrm{bday}\left(A\right)$$
27		elun1	$$⊢\mathrm{bday}\left(a\right)\in \mathrm{bday}\left(A\right)\to \mathrm{bday}\left(a\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)$$
28	26 27	syl	$$⊢\left(\phi \wedge a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right)\to \mathrm{bday}\left(a\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)$$
29	24 28	eqeltrid	$$⊢\left(\phi \wedge a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right)\to \mathrm{bday}\left(a\right)\cup \mathrm{bday}\left(0_s\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)$$
30	15 18 20 29	negsproplem1	$$⊢\left(\phi \wedge a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right)\to \left({+}_s\left(a\right)\in \mathrm{No}\wedge \left(a{<}_s{0}_s\to {+}_s\left(0_s\right){<}_s{+}_s\left(a\right)\right)\right)$$
31	30	simpld	$$⊢\left(\phi \wedge a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right)\to {+}_s\left(a\right)\in \mathrm{No}$$
32	31	ralrimiva	$$⊢\phi \to \forall a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right){+}_s\left(a\right)\in \mathrm{No}$$
33	3	fndmi	$$⊢\mathrm{dom}{+}_s=\mathrm{No}$$
34	16 33	sseqtrri	$$⊢\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\subseteq \mathrm{dom}{+}_s$$
35		funimass4	$$⊢\left(\mathrm{Fun}{+}_s\wedge \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\subseteq \mathrm{dom}{+}_s\right)\to \left({+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right]\subseteq \mathrm{No}\leftrightarrow \forall a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right){+}_s\left(a\right)\in \mathrm{No}\right)$$
36	5 34 35	mp2an	$$⊢{+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right]\subseteq \mathrm{No}\leftrightarrow \forall a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right){+}_s\left(a\right)\in \mathrm{No}$$
37	32 36	sylibr	$$⊢\phi \to {+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right]\subseteq \mathrm{No}$$
38	14 37	sstrid	$$⊢\phi \to {+}_s\left[R\left(A\right)\right]\subseteq \mathrm{No}$$
39		leftssold	$$⊢L\left(A\right)\subseteq \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
40		imass2	$$⊢L\left(A\right)\subseteq \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\to {+}_s\left[L\left(A\right)\right]\subseteq {+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right]$$
41	39 40	ax-mp	$$⊢{+}_s\left[L\left(A\right)\right]\subseteq {+}_s\left[\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right]$$
42	41 37	sstrid	$$⊢\phi \to {+}_s\left[L\left(A\right)\right]\subseteq \mathrm{No}$$
43		rightssno	$$⊢R\left(A\right)\subseteq \mathrm{No}$$
44		fvelimab	Could not format ( ( -us Fn No /\ ( _Right ` A ) C_ No ) -> ( a e. ( -us " ( _Right ` A ) ) <-> E. xR e. ( _Right ` A ) ( -us ` xR ) = a ) ) : No typesetting found for |- ( ( -us Fn No /\ ( _Right ` A ) C_ No ) -> ( a e. ( -us " ( _Right ` A ) ) <-> E. xR e. ( _Right ` A ) ( -us ` xR ) = a ) ) with typecode |-
45	3 43 44	mp2an	Could not format ( a e. ( -us " ( _Right ` A ) ) <-> E. xR e. ( _Right ` A ) ( -us ` xR ) = a ) : No typesetting found for |- ( a e. ( -us " ( _Right ` A ) ) <-> E. xR e. ( _Right ` A ) ( -us ` xR ) = a ) with typecode |-
46		leftssno	$$⊢L\left(A\right)\subseteq \mathrm{No}$$
47		fvelimab	Could not format ( ( -us Fn No /\ ( _Left ` A ) C_ No ) -> ( b e. ( -us " ( _Left ` A ) ) <-> E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) ) : No typesetting found for |- ( ( -us Fn No /\ ( _Left ` A ) C_ No ) -> ( b e. ( -us " ( _Left ` A ) ) <-> E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) ) with typecode |-
48	3 46 47	mp2an	Could not format ( b e. ( -us " ( _Left ` A ) ) <-> E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) : No typesetting found for |- ( b e. ( -us " ( _Left ` A ) ) <-> E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) with typecode |-
49	45 48	anbi12i	Could not format ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) <-> ( E. xR e. ( _Right ` A ) ( -us ` xR ) = a /\ E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) ) : No typesetting found for |- ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) <-> ( E. xR e. ( _Right ` A ) ( -us ` xR ) = a /\ E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) ) with typecode |-
50		reeanv	Could not format ( E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) <-> ( E. xR e. ( _Right ` A ) ( -us ` xR ) = a /\ E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) ) : No typesetting found for |- ( E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) <-> ( E. xR e. ( _Right ` A ) ( -us ` xR ) = a /\ E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) ) with typecode |-
51	49 50	bitr4i	Could not format ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) <-> E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) ) : No typesetting found for |- ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) <-> E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) ) with typecode |-
52		lltropt	$$⊢L\left(A\right){\ll }_{s}R\left(A\right)$$
53	52	a1i	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( _Left ` A ) < ( _Left ` A ) <
54		simprr	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. ( _Left ` A ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. ( _Left ` A ) ) with typecode |-
55		simprl	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. ( _Right ` A ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. ( _Right ` A ) ) with typecode |-
56	53 54 55	ssltsepcd	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL xL
57	1	adantr	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
58	46	sseli	Could not format ( xL e. ( _Left ` A ) -> xL e. No ) : No typesetting found for |- ( xL e. ( _Left ` A ) -> xL e. No ) with typecode |-
59	58	ad2antll	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. No ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. No ) with typecode |-
60	43	sseli	Could not format ( xR e. ( _Right ` A ) -> xR e. No ) : No typesetting found for |- ( xR e. ( _Right ` A ) -> xR e. No ) with typecode |-
61	60	adantr	Could not format ( ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) -> xR e. No ) : No typesetting found for |- ( ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) -> xR e. No ) with typecode |-
62	61	adantl	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. No ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. No ) with typecode |-
63	39	sseli	Could not format ( xL e. ( _Left ` A ) -> xL e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( xL e. ( _Left ` A ) -> xL e. ( _Old ` ( bday ` A ) ) ) with typecode |-
64	63	ad2antll	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. ( _Old ` ( bday ` A ) ) ) with typecode |-
65		oldbdayim	Could not format ( xL e. ( _Old ` ( bday ` A ) ) -> ( bday ` xL ) e. ( bday ` A ) ) : No typesetting found for |- ( xL e. ( _Old ` ( bday ` A ) ) -> ( bday ` xL ) e. ( bday ` A ) ) with typecode |-
66	64 65	syl	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( bday ` xL ) e. ( bday ` A ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( bday ` xL ) e. ( bday ` A ) ) with typecode |-
67	12	a1i	$$⊢\phi \to R\left(A\right)\subseteq \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
68	67	sselda	Could not format ( ( ph /\ xR e. ( _Right ` A ) ) -> xR e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ( ph /\ xR e. ( _Right ` A ) ) -> xR e. ( _Old ` ( bday ` A ) ) ) with typecode |-
69	68	adantrr	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. ( _Old ` ( bday ` A ) ) ) with typecode |-
70		oldbdayim	Could not format ( xR e. ( _Old ` ( bday ` A ) ) -> ( bday ` xR ) e. ( bday ` A ) ) : No typesetting found for |- ( xR e. ( _Old ` ( bday ` A ) ) -> ( bday ` xR ) e. ( bday ` A ) ) with typecode |-
71	69 70	syl	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( bday ` xR ) e. ( bday ` A ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( bday ` xR ) e. ( bday ` A ) ) with typecode |-
72		bdayelon	Could not format ( bday ` xL ) e. On : No typesetting found for |- ( bday ` xL ) e. On with typecode |-
73		bdayelon	Could not format ( bday ` xR ) e. On : No typesetting found for |- ( bday ` xR ) e. On with typecode |-
74		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
75		onunel	Could not format ( ( ( bday ` xL ) e. On /\ ( bday ` xR ) e. On /\ ( bday ` A ) e. On ) -> ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) <-> ( ( bday ` xL ) e. ( bday ` A ) /\ ( bday ` xR ) e. ( bday ` A ) ) ) ) : No typesetting found for |- ( ( ( bday ` xL ) e. On /\ ( bday ` xR ) e. On /\ ( bday ` A ) e. On ) -> ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) <-> ( ( bday ` xL ) e. ( bday ` A ) /\ ( bday ` xR ) e. ( bday ` A ) ) ) ) with typecode |-
76	72 73 74 75	mp3an	Could not format ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) <-> ( ( bday ` xL ) e. ( bday ` A ) /\ ( bday ` xR ) e. ( bday ` A ) ) ) : No typesetting found for |- ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) <-> ( ( bday ` xL ) e. ( bday ` A ) /\ ( bday ` xR ) e. ( bday ` A ) ) ) with typecode |-
77	66 71 76	sylanbrc	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) ) with typecode |-
78		elun1	Could not format ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) : No typesetting found for |- ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) with typecode |-
79	77 78	syl	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) with typecode |-
80	57 59 62 79	negsproplem1	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( -us ` xL ) e. No /\ ( xL ( -us ` xR ) ( ( -us ` xL ) e. No /\ ( xL ( -us ` xR )
81	80	simprd	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( xL ( -us ` xR ) ( xL ( -us ` xR )
82	56 81	mpd	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( -us ` xR ) ( -us ` xR )
83		breq12	Could not format ( ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> ( ( -us ` xR ) a ( ( -us ` xR ) a
84	82 83	syl5ibcom	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> a ( ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> a
85	84	rexlimdvva	Could not format ( ph -> ( E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> a ( E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> a
86	51 85	biimtrid	$$⊢\phi \to \left(\left(a\in {+}_s\left[R\left(A\right)\right]\wedge b\in {+}_s\left[L\left(A\right)\right]\right)\to a{<}_{s}b\right)$$
87	86	3impib	$$⊢\left(\phi \wedge a\in {+}_s\left[R\left(A\right)\right]\wedge b\in {+}_s\left[L\left(A\right)\right]\right)\to a{<}_{s}b$$
88	8 11 38 42 87	ssltd	$$⊢\phi \to {+}_s\left[R\left(A\right)\right]{\ll }_s{+}_s\left[L\left(A\right)\right]$$