Theorem precsexlem7

Description: Lemma for surreal reciprocal. Show that R 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	precsexlem7	$$⊢\left(I\in \mathrm{\omega }\wedge J\in \mathrm{\omega }\wedge I\subseteq J\right)\to R\left(I\right)\subseteq R\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 R\left(I{+}_{𝑜}k\right)=R\left(I{+}_{𝑜}\varnothing \right)$$
7	6	sseq2d	$$⊢k=\varnothing \to \left(R\left(I\right)\subseteq R\left(I{+}_{𝑜}k\right)\leftrightarrow R\left(I\right)\subseteq R\left(I{+}_{𝑜}\varnothing \right)\right)$$
8		oveq2	$$⊢k=j\to I{+}_{𝑜}k=I{+}_{𝑜}j$$
9	8	fveq2d	$$⊢k=j\to R\left(I{+}_{𝑜}k\right)=R\left(I{+}_{𝑜}j\right)$$
10	9	sseq2d	$$⊢k=j\to \left(R\left(I\right)\subseteq R\left(I{+}_{𝑜}k\right)\leftrightarrow R\left(I\right)\subseteq R\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 R\left(I{+}_{𝑜}k\right)=R\left(I{+}_{𝑜}\mathrm{suc}j\right)$$
13	12	sseq2d	$$⊢k=\mathrm{suc}j\to \left(R\left(I\right)\subseteq R\left(I{+}_{𝑜}k\right)\leftrightarrow R\left(I\right)\subseteq R\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 R\left(I{+}_{𝑜}\varnothing \right)=R\left(I\right)$$
16	15	eqimsscd	$$⊢I\in \mathrm{\omega }\to R\left(I\right)\subseteq R\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 ( R ` ( I +o j ) ) C_ ( ( R ` ( I +o j ) ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
19	1 2 3	precsexlem5	Could not format ( ( I +o j ) e. _om -> ( R ` suc ( I +o j ) ) = ( ( R ` ( I +o j ) ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( R ` suc ( I +o j ) ) = ( ( R ` ( I +o j ) ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
20	18 19	sseqtrrid	$$⊢I{+}_{𝑜}j\in \mathrm{\omega }\to R\left(I{+}_{𝑜}j\right)\subseteq R\left(\mathrm{suc}\left(I{+}_{𝑜}j\right)\right)$$
21	17 20	syl	$$⊢\left(I\in \mathrm{\omega }\wedge j\in \mathrm{\omega }\right)\to R\left(I{+}_{𝑜}j\right)\subseteq R\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 R\left(I{+}_{𝑜}\mathrm{suc}j\right)=R\left(\mathrm{suc}\left(I{+}_{𝑜}j\right)\right)$$
24	21 23	sseqtrrd	$$⊢\left(I\in \mathrm{\omega }\wedge j\in \mathrm{\omega }\right)\to R\left(I{+}_{𝑜}j\right)\subseteq R\left(I{+}_{𝑜}\mathrm{suc}j\right)$$
25		sstr2	$$⊢R\left(I\right)\subseteq R\left(I{+}_{𝑜}j\right)\to \left(R\left(I{+}_{𝑜}j\right)\subseteq R\left(I{+}_{𝑜}\mathrm{suc}j\right)\to R\left(I\right)\subseteq R\left(I{+}_{𝑜}\mathrm{suc}j\right)\right)$$
26	24 25	syl5com	$$⊢\left(I\in \mathrm{\omega }\wedge j\in \mathrm{\omega }\right)\to \left(R\left(I\right)\subseteq R\left(I{+}_{𝑜}j\right)\to R\left(I\right)\subseteq R\left(I{+}_{𝑜}\mathrm{suc}j\right)\right)$$
27	26	expcom	$$⊢j\in \mathrm{\omega }\to \left(I\in \mathrm{\omega }\to \left(R\left(I\right)\subseteq R\left(I{+}_{𝑜}j\right)\to R\left(I\right)\subseteq R\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 R\left(I\right)\subseteq R\left(I{+}_{𝑜}k\right)\right)$$
29	28	impcom	$$⊢\left(I\in \mathrm{\omega }\wedge k\in \mathrm{\omega }\right)\to R\left(I\right)\subseteq R\left(I{+}_{𝑜}k\right)$$
30		fveq2	$$⊢I{+}_{𝑜}k=J\to R\left(I{+}_{𝑜}k\right)=R\left(J\right)$$
31	30	sseq2d	$$⊢I{+}_{𝑜}k=J\to \left(R\left(I\right)\subseteq R\left(I{+}_{𝑜}k\right)\leftrightarrow R\left(I\right)\subseteq R\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 R\left(I\right)\subseteq R\left(J\right)\right)$$
33	32	rexlimdva	$$⊢I\in \mathrm{\omega }\to \left(\exists k\in \mathrm{\omega }I{+}_{𝑜}k=J\to R\left(I\right)\subseteq R\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 R\left(I\right)\subseteq R\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 R\left(I\right)\subseteq R\left(J\right)\right)$$
36	35	3impia	$$⊢\left(I\in \mathrm{\omega }\wedge J\in \mathrm{\omega }\wedge I\subseteq J\right)\to R\left(I\right)\subseteq R\left(J\right)$$