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	$⊢ (I \in ω \land J \in ω \land I \subseteq J) \to R (I) \subseteq R (J)$

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	$⊢ (I \in ω \land J \in ω) \to (I \subseteq J \leftrightarrow \exists k \in ω I +_{𝑜} k = J)$
5		oveq2	$⊢ k = \emptyset \to I +_{𝑜} k = I +_{𝑜} \emptyset$
6	5	fveq2d	$⊢ k = \emptyset \to R (I +_{𝑜} k) = R (I +_{𝑜} \emptyset)$
7	6	sseq2d	$⊢ k = \emptyset \to (R (I) \subseteq R (I +_{𝑜} k) \leftrightarrow R (I) \subseteq R (I +_{𝑜} \emptyset))$
8		oveq2	$⊢ k = j \to I +_{𝑜} k = I +_{𝑜} j$
9	8	fveq2d	$⊢ k = j \to R (I +_{𝑜} k) = R (I +_{𝑜} j)$
10	9	sseq2d	$⊢ k = j \to (R (I) \subseteq R (I +_{𝑜} k) \leftrightarrow R (I) \subseteq R (I +_{𝑜} j))$
11		oveq2	$⊢ k = suc j \to I +_{𝑜} k = I +_{𝑜} suc j$
12	11	fveq2d	$⊢ k = suc j \to R (I +_{𝑜} k) = R (I +_{𝑜} suc j)$
13	12	sseq2d	$⊢ k = suc j \to (R (I) \subseteq R (I +_{𝑜} k) \leftrightarrow R (I) \subseteq R (I +_{𝑜} suc j))$
14		nna0	$⊢ I \in ω \to I +_{𝑜} \emptyset = I$
15	14	fveq2d	$⊢ I \in ω \to R (I +_{𝑜} \emptyset) = R (I)$
16	15	eqimsscd	$⊢ I \in ω \to R (I) \subseteq R (I +_{𝑜} \emptyset)$
17		nnacl	$⊢ (I \in ω \land j \in ω) \to I +_{𝑜} j \in ω$
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 ω \to R (I +_{𝑜} j) \subseteq R (suc (I +_{𝑜} j))$
21	17 20	syl	$⊢ (I \in ω \land j \in ω) \to R (I +_{𝑜} j) \subseteq R (suc (I +_{𝑜} j))$
22		nnasuc	$⊢ (I \in ω \land j \in ω) \to I +_{𝑜} suc j = suc (I +_{𝑜} j)$
23	22	fveq2d	$⊢ (I \in ω \land j \in ω) \to R (I +_{𝑜} suc j) = R (suc (I +_{𝑜} j))$
24	21 23	sseqtrrd	$⊢ (I \in ω \land j \in ω) \to R (I +_{𝑜} j) \subseteq R (I +_{𝑜} suc j)$
25		sstr2	$⊢ R (I) \subseteq R (I +_{𝑜} j) \to (R (I +_{𝑜} j) \subseteq R (I +_{𝑜} suc j) \to R (I) \subseteq R (I +_{𝑜} suc j))$
26	24 25	syl5com	$⊢ (I \in ω \land j \in ω) \to (R (I) \subseteq R (I +_{𝑜} j) \to R (I) \subseteq R (I +_{𝑜} suc j))$
27	26	expcom	$⊢ j \in ω \to (I \in ω \to (R (I) \subseteq R (I +_{𝑜} j) \to R (I) \subseteq R (I +_{𝑜} suc j)))$
28	7 10 13 16 27	finds2	$⊢ k \in ω \to (I \in ω \to R (I) \subseteq R (I +_{𝑜} k))$
29	28	impcom	$⊢ (I \in ω \land k \in ω) \to R (I) \subseteq R (I +_{𝑜} k)$
30		fveq2	$⊢ I +_{𝑜} k = J \to R (I +_{𝑜} k) = R (J)$
31	30	sseq2d	$⊢ I +_{𝑜} k = J \to (R (I) \subseteq R (I +_{𝑜} k) \leftrightarrow R (I) \subseteq R (J))$
32	29 31	syl5ibcom	$⊢ (I \in ω \land k \in ω) \to (I +_{𝑜} k = J \to R (I) \subseteq R (J))$
33	32	rexlimdva	$⊢ I \in ω \to (\exists k \in ω I +_{𝑜} k = J \to R (I) \subseteq R (J))$
34	33	adantr	$⊢ (I \in ω \land J \in ω) \to (\exists k \in ω I +_{𝑜} k = J \to R (I) \subseteq R (J))$
35	4 34	sylbid	$⊢ (I \in ω \land J \in ω) \to (I \subseteq J \to R (I) \subseteq R (J))$
36	35	3impia	$⊢ (I \in ω \land J \in ω \land I \subseteq J) \to R (I) \subseteq R (J)$

Metamath Proof Explorer

Theorem precsexlem7

Proof