Metamath Proof Explorer

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 
|- 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 } , (/) >. )
precsexlem.2 
|- L = ( 1st o. F )
precsexlem.3 
|- R = ( 2nd o. F )
Assertion precsexlem7 
|- ( ( I e. _om /\ J e. _om /\ I C_ J ) -> ( R ` I ) C_ ( R ` J ) )

Proof

Step Hyp Ref Expression
1 precsexlem.1 
 |-  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 } , (/) >. )
2 precsexlem.2 
 |-  L = ( 1st o. F )
3 precsexlem.3 
 |-  R = ( 2nd o. F )
4 nnawordex 
 |-  ( ( I e. _om /\ J e. _om ) -> ( I C_ J <-> E. k e. _om ( I +o k ) = J ) )
5 oveq2 
 |-  ( k = (/) -> ( I +o k ) = ( I +o (/) ) )
6 5 fveq2d 
 |-  ( k = (/) -> ( R ` ( I +o k ) ) = ( R ` ( I +o (/) ) ) )
7 6 sseq2d 
 |-  ( k = (/) -> ( ( R ` I ) C_ ( R ` ( I +o k ) ) <-> ( R ` I ) C_ ( R ` ( I +o (/) ) ) ) )
8 oveq2 
 |-  ( k = j -> ( I +o k ) = ( I +o j ) )
9 8 fveq2d 
 |-  ( k = j -> ( R ` ( I +o k ) ) = ( R ` ( I +o j ) ) )
10 9 sseq2d 
 |-  ( k = j -> ( ( R ` I ) C_ ( R ` ( I +o k ) ) <-> ( R ` I ) C_ ( R ` ( I +o j ) ) ) )
11 oveq2 
 |-  ( k = suc j -> ( I +o k ) = ( I +o suc j ) )
12 11 fveq2d 
 |-  ( k = suc j -> ( R ` ( I +o k ) ) = ( R ` ( I +o suc j ) ) )
13 12 sseq2d 
 |-  ( k = suc j -> ( ( R ` I ) C_ ( R ` ( I +o k ) ) <-> ( R ` I ) C_ ( R ` ( I +o suc j ) ) ) )
14 nna0 
 |-  ( I e. _om -> ( I +o (/) ) = I )
15 14 fveq2d 
 |-  ( I e. _om -> ( R ` ( I +o (/) ) ) = ( R ` I ) )
16 15 eqimsscd 
 |-  ( I e. _om -> ( R ` I ) C_ ( R ` ( I +o (/) ) ) )
17 nnacl 
 |-  ( ( I e. _om /\ j e. _om ) -> ( I +o j ) e. _om )
18 ssun1 
 |-  ( R ` ( I +o j ) ) C_ ( ( R ` ( I +o j ) ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
19 1 2 3 precsexlem5 
 |-  ( ( I +o j ) e. _om -> ( R ` suc ( I +o j ) ) = ( ( R ` ( I +o j ) ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
20 18 19 sseqtrrid 
 |-  ( ( I +o j ) e. _om -> ( R ` ( I +o j ) ) C_ ( R ` suc ( I +o j ) ) )
21 17 20 syl 
 |-  ( ( I e. _om /\ j e. _om ) -> ( R ` ( I +o j ) ) C_ ( R ` suc ( I +o j ) ) )
22 nnasuc 
 |-  ( ( I e. _om /\ j e. _om ) -> ( I +o suc j ) = suc ( I +o j ) )
23 22 fveq2d 
 |-  ( ( I e. _om /\ j e. _om ) -> ( R ` ( I +o suc j ) ) = ( R ` suc ( I +o j ) ) )
24 21 23 sseqtrrd 
 |-  ( ( I e. _om /\ j e. _om ) -> ( R ` ( I +o j ) ) C_ ( R ` ( I +o suc j ) ) )
25 sstr2 
 |-  ( ( R ` I ) C_ ( R ` ( I +o j ) ) -> ( ( R ` ( I +o j ) ) C_ ( R ` ( I +o suc j ) ) -> ( R ` I ) C_ ( R ` ( I +o suc j ) ) ) )
26 24 25 syl5com 
 |-  ( ( I e. _om /\ j e. _om ) -> ( ( R ` I ) C_ ( R ` ( I +o j ) ) -> ( R ` I ) C_ ( R ` ( I +o suc j ) ) ) )
27 26 expcom 
 |-  ( j e. _om -> ( I e. _om -> ( ( R ` I ) C_ ( R ` ( I +o j ) ) -> ( R ` I ) C_ ( R ` ( I +o suc j ) ) ) ) )
28 7 10 13 16 27 finds2 
 |-  ( k e. _om -> ( I e. _om -> ( R ` I ) C_ ( R ` ( I +o k ) ) ) )
29 28 impcom 
 |-  ( ( I e. _om /\ k e. _om ) -> ( R ` I ) C_ ( R ` ( I +o k ) ) )
30 fveq2 
 |-  ( ( I +o k ) = J -> ( R ` ( I +o k ) ) = ( R ` J ) )
31 30 sseq2d 
 |-  ( ( I +o k ) = J -> ( ( R ` I ) C_ ( R ` ( I +o k ) ) <-> ( R ` I ) C_ ( R ` J ) ) )
32 29 31 syl5ibcom 
 |-  ( ( I e. _om /\ k e. _om ) -> ( ( I +o k ) = J -> ( R ` I ) C_ ( R ` J ) ) )
33 32 rexlimdva 
 |-  ( I e. _om -> ( E. k e. _om ( I +o k ) = J -> ( R ` I ) C_ ( R ` J ) ) )
34 33 adantr 
 |-  ( ( I e. _om /\ J e. _om ) -> ( E. k e. _om ( I +o k ) = J -> ( R ` I ) C_ ( R ` J ) ) )
35 4 34 sylbid 
 |-  ( ( I e. _om /\ J e. _om ) -> ( I C_ J -> ( R ` I ) C_ ( R ` J ) ) )
36 35 3impia 
 |-  ( ( I e. _om /\ J e. _om /\ I C_ J ) -> ( R ` I ) C_ ( R ` J ) )