Theorem precsexlem6

Description: Lemma for surreal reciprocal. Show that L is non-strictly increasing in its argument. (Contributed by Scott Fenton, 15-Mar-2025)

	Ref	Expression
Hypotheses	precsexlem.1	No typesetting found for |- F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) with typecode |-
	precsexlem.2	$$⊢L=1^{st}\circ F$$
	precsexlem.3	$$⊢R=2^{nd}\circ F$$
Assertion	precsexlem6	$$⊢\left(I\in \mathrm{\omega }\wedge J\in \mathrm{\omega }\wedge I\subseteq J\right)\to L\left(I\right)\subseteq L\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		precsexlem.1	Could not format F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) : No typesetting found for |- F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) with typecode |-
2		precsexlem.2	$$⊢L=1^{st}\circ F$$
3		precsexlem.3	$$⊢R=2^{nd}\circ F$$
4		nnawordex	$$⊢\left(I\in \mathrm{\omega }\wedge J\in \mathrm{\omega }\right)\to \left(I\subseteq J\leftrightarrow \exists k\in \mathrm{\omega }I{+}_{𝑜}k=J\right)$$
5		oveq2	$$⊢k=\varnothing \to I{+}_{𝑜}k=I{+}_{𝑜}\varnothing$$
6	5	fveq2d	$$⊢k=\varnothing \to L\left(I{+}_{𝑜}k\right)=L\left(I{+}_{𝑜}\varnothing \right)$$
7	6	sseq2d	$$⊢k=\varnothing \to \left(L\left(I\right)\subseteq L\left(I{+}_{𝑜}k\right)\leftrightarrow L\left(I\right)\subseteq L\left(I{+}_{𝑜}\varnothing \right)\right)$$
8		oveq2	$$⊢k=j\to I{+}_{𝑜}k=I{+}_{𝑜}j$$
9	8	fveq2d	$$⊢k=j\to L\left(I{+}_{𝑜}k\right)=L\left(I{+}_{𝑜}j\right)$$
10	9	sseq2d	$$⊢k=j\to \left(L\left(I\right)\subseteq L\left(I{+}_{𝑜}k\right)\leftrightarrow L\left(I\right)\subseteq L\left(I{+}_{𝑜}j\right)\right)$$
11		oveq2	$$⊢k=\mathrm{suc}j\to I{+}_{𝑜}k=I{+}_{𝑜}\mathrm{suc}j$$
12	11	fveq2d	$$⊢k=\mathrm{suc}j\to L\left(I{+}_{𝑜}k\right)=L\left(I{+}_{𝑜}\mathrm{suc}j\right)$$
13	12	sseq2d	$$⊢k=\mathrm{suc}j\to \left(L\left(I\right)\subseteq L\left(I{+}_{𝑜}k\right)\leftrightarrow L\left(I\right)\subseteq L\left(I{+}_{𝑜}\mathrm{suc}j\right)\right)$$
14		nna0	$$⊢I\in \mathrm{\omega }\to I{+}_{𝑜}\varnothing =I$$
15	14	fveq2d	$$⊢I\in \mathrm{\omega }\to L\left(I{+}_{𝑜}\varnothing \right)=L\left(I\right)$$
16	15	eqimsscd	$$⊢I\in \mathrm{\omega }\to L\left(I\right)\subseteq L\left(I{+}_{𝑜}\varnothing \right)$$
17		nnacl	$$⊢\left(I\in \mathrm{\omega }\wedge j\in \mathrm{\omega }\right)\to I{+}_{𝑜}j\in \mathrm{\omega }$$
18		ssun1	Could not format ( L ` ( I +o j ) ) C_ ( ( L ` ( I +o j ) ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` ( I +o j ) ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
19	1 2 3	precsexlem4	Could not format ( ( I +o j ) e. _om -> ( L ` suc ( I +o j ) ) = ( ( L ` ( I +o j ) ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` ( I +o j ) ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( L ` suc ( I +o j ) ) = ( ( L ` ( I +o j ) ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` ( I +o j ) ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
20	18 19	sseqtrrid	$$⊢I{+}_{𝑜}j\in \mathrm{\omega }\to L\left(I{+}_{𝑜}j\right)\subseteq L\left(\mathrm{suc}\left(I{+}_{𝑜}j\right)\right)$$
21	17 20	syl	$$⊢\left(I\in \mathrm{\omega }\wedge j\in \mathrm{\omega }\right)\to L\left(I{+}_{𝑜}j\right)\subseteq L\left(\mathrm{suc}\left(I{+}_{𝑜}j\right)\right)$$
22		nnasuc	$$⊢\left(I\in \mathrm{\omega }\wedge j\in \mathrm{\omega }\right)\to I{+}_{𝑜}\mathrm{suc}j=\mathrm{suc}\left(I{+}_{𝑜}j\right)$$
23	22	fveq2d	$$⊢\left(I\in \mathrm{\omega }\wedge j\in \mathrm{\omega }\right)\to L\left(I{+}_{𝑜}\mathrm{suc}j\right)=L\left(\mathrm{suc}\left(I{+}_{𝑜}j\right)\right)$$
24	21 23	sseqtrrd	$$⊢\left(I\in \mathrm{\omega }\wedge j\in \mathrm{\omega }\right)\to L\left(I{+}_{𝑜}j\right)\subseteq L\left(I{+}_{𝑜}\mathrm{suc}j\right)$$
25		sstr2	$$⊢L\left(I\right)\subseteq L\left(I{+}_{𝑜}j\right)\to \left(L\left(I{+}_{𝑜}j\right)\subseteq L\left(I{+}_{𝑜}\mathrm{suc}j\right)\to L\left(I\right)\subseteq L\left(I{+}_{𝑜}\mathrm{suc}j\right)\right)$$
26	24 25	syl5com	$$⊢\left(I\in \mathrm{\omega }\wedge j\in \mathrm{\omega }\right)\to \left(L\left(I\right)\subseteq L\left(I{+}_{𝑜}j\right)\to L\left(I\right)\subseteq L\left(I{+}_{𝑜}\mathrm{suc}j\right)\right)$$
27	26	expcom	$$⊢j\in \mathrm{\omega }\to \left(I\in \mathrm{\omega }\to \left(L\left(I\right)\subseteq L\left(I{+}_{𝑜}j\right)\to L\left(I\right)\subseteq L\left(I{+}_{𝑜}\mathrm{suc}j\right)\right)\right)$$
28	7 10 13 16 27	finds2	$$⊢k\in \mathrm{\omega }\to \left(I\in \mathrm{\omega }\to L\left(I\right)\subseteq L\left(I{+}_{𝑜}k\right)\right)$$
29	28	impcom	$$⊢\left(I\in \mathrm{\omega }\wedge k\in \mathrm{\omega }\right)\to L\left(I\right)\subseteq L\left(I{+}_{𝑜}k\right)$$
30		fveq2	$$⊢I{+}_{𝑜}k=J\to L\left(I{+}_{𝑜}k\right)=L\left(J\right)$$
31	30	sseq2d	$$⊢I{+}_{𝑜}k=J\to \left(L\left(I\right)\subseteq L\left(I{+}_{𝑜}k\right)\leftrightarrow L\left(I\right)\subseteq L\left(J\right)\right)$$
32	29 31	syl5ibcom	$$⊢\left(I\in \mathrm{\omega }\wedge k\in \mathrm{\omega }\right)\to \left(I{+}_{𝑜}k=J\to L\left(I\right)\subseteq L\left(J\right)\right)$$
33	32	rexlimdva	$$⊢I\in \mathrm{\omega }\to \left(\exists k\in \mathrm{\omega }I{+}_{𝑜}k=J\to L\left(I\right)\subseteq L\left(J\right)\right)$$
34	33	adantr	$$⊢\left(I\in \mathrm{\omega }\wedge J\in \mathrm{\omega }\right)\to \left(\exists k\in \mathrm{\omega }I{+}_{𝑜}k=J\to L\left(I\right)\subseteq L\left(J\right)\right)$$
35	4 34	sylbid	$$⊢\left(I\in \mathrm{\omega }\wedge J\in \mathrm{\omega }\right)\to \left(I\subseteq J\to L\left(I\right)\subseteq L\left(J\right)\right)$$
36	35	3impia	$$⊢\left(I\in \mathrm{\omega }\wedge J\in \mathrm{\omega }\wedge I\subseteq J\right)\to L\left(I\right)\subseteq L\left(J\right)$$