Metamath Proof Explorer

Theorem precsexlem10

Description: Lemma for surreal reciprocal. Show that the union of the left sets is less than the union of the right sets. Note that this is the first theorem in the surreal numbers to require the axiom of infinity. (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 )
precsexlem.4 
|- ( ph -> A e. No )
precsexlem.5 
|- ( ph -> 0s
precsexlem.6 
|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
Assertion precsexlem10 
|- ( ph -> U. ( L " _om ) <

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 precsexlem.4 
 |-  ( ph -> A e. No )
5 precsexlem.5 
 |-  ( ph -> 0s
6 precsexlem.6 
 |-  ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
7 fo1st 
 |-  1st : _V -onto-> _V
8 fofun 
 |-  ( 1st : _V -onto-> _V -> Fun 1st )
9 7 8 ax-mp 
 |-  Fun 1st
10 rdgfun 
 |-  Fun 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 } , (/) >. )
11 1 funeqi 
 |-  ( Fun F <-> Fun 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 } , (/) >. ) )
12 10 11 mpbir 
 |-  Fun F
13 funco 
 |-  ( ( Fun 1st /\ Fun F ) -> Fun ( 1st o. F ) )
14 9 12 13 mp2an 
 |-  Fun ( 1st o. F )
15 2 funeqi 
 |-  ( Fun L <-> Fun ( 1st o. F ) )
16 14 15 mpbir 
 |-  Fun L
17 dcomex 
 |-  _om e. _V
18 17 funimaex 
 |-  ( Fun L -> ( L " _om ) e. _V )
19 16 18 ax-mp 
 |-  ( L " _om ) e. _V
20 19 uniex 
 |-  U. ( L " _om ) e. _V
21 20 a1i 
 |-  ( ph -> U. ( L " _om ) e. _V )
22 fo2nd 
 |-  2nd : _V -onto-> _V
23 fofun 
 |-  ( 2nd : _V -onto-> _V -> Fun 2nd )
24 22 23 ax-mp 
 |-  Fun 2nd
25 funco 
 |-  ( ( Fun 2nd /\ Fun F ) -> Fun ( 2nd o. F ) )
26 24 12 25 mp2an 
 |-  Fun ( 2nd o. F )
27 3 funeqi 
 |-  ( Fun R <-> Fun ( 2nd o. F ) )
28 26 27 mpbir 
 |-  Fun R
29 17 funimaex 
 |-  ( Fun R -> ( R " _om ) e. _V )
30 28 29 ax-mp 
 |-  ( R " _om ) e. _V
31 30 uniex 
 |-  U. ( R " _om ) e. _V
32 31 a1i 
 |-  ( ph -> U. ( R " _om ) e. _V )
33 funiunfv 
 |-  ( Fun L -> U_ i e. _om ( L ` i ) = U. ( L " _om ) )
34 16 33 ax-mp 
 |-  U_ i e. _om ( L ` i ) = U. ( L " _om )
35 1 2 3 4 5 6 precsexlem8 
 |-  ( ( ph /\ i e. _om ) -> ( ( L ` i ) C_ No /\ ( R ` i ) C_ No ) )
36 35 simpld 
 |-  ( ( ph /\ i e. _om ) -> ( L ` i ) C_ No )
37 36 iunssd 
 |-  ( ph -> U_ i e. _om ( L ` i ) C_ No )
38 34 37 eqsstrrid 
 |-  ( ph -> U. ( L " _om ) C_ No )
39 funiunfv 
 |-  ( Fun R -> U_ i e. _om ( R ` i ) = U. ( R " _om ) )
40 28 39 ax-mp 
 |-  U_ i e. _om ( R ` i ) = U. ( R " _om )
41 35 simprd 
 |-  ( ( ph /\ i e. _om ) -> ( R ` i ) C_ No )
42 41 iunssd 
 |-  ( ph -> U_ i e. _om ( R ` i ) C_ No )
43 40 42 eqsstrrid 
 |-  ( ph -> U. ( R " _om ) C_ No )
44 34 eleq2i 
 |-  ( b e. U_ i e. _om ( L ` i ) <-> b e. U. ( L " _om ) )
45 eliun 
 |-  ( b e. U_ i e. _om ( L ` i ) <-> E. i e. _om b e. ( L ` i ) )
46 44 45 bitr3i 
 |-  ( b e. U. ( L " _om ) <-> E. i e. _om b e. ( L ` i ) )
47 funiunfv 
 |-  ( Fun R -> U_ j e. _om ( R ` j ) = U. ( R " _om ) )
48 28 47 ax-mp 
 |-  U_ j e. _om ( R ` j ) = U. ( R " _om )
49 48 eleq2i 
 |-  ( c e. U_ j e. _om ( R ` j ) <-> c e. U. ( R " _om ) )
50 eliun 
 |-  ( c e. U_ j e. _om ( R ` j ) <-> E. j e. _om c e. ( R ` j ) )
51 49 50 bitr3i 
 |-  ( c e. U. ( R " _om ) <-> E. j e. _om c e. ( R ` j ) )
52 46 51 anbi12i 
 |-  ( ( b e. U. ( L " _om ) /\ c e. U. ( R " _om ) ) <-> ( E. i e. _om b e. ( L ` i ) /\ E. j e. _om c e. ( R ` j ) ) )
53 reeanv 
 |-  ( E. i e. _om E. j e. _om ( b e. ( L ` i ) /\ c e. ( R ` j ) ) <-> ( E. i e. _om b e. ( L ` i ) /\ E. j e. _om c e. ( R ` j ) ) )
54 52 53 bitr4i 
 |-  ( ( b e. U. ( L " _om ) /\ c e. U. ( R " _om ) ) <-> E. i e. _om E. j e. _om ( b e. ( L ` i ) /\ c e. ( R ` j ) ) )
55 omun 
 |-  ( ( i e. _om /\ j e. _om ) -> ( i u. j ) e. _om )
56 ssun1 
 |-  i C_ ( i u. j )
57 1 2 3 precsexlem6 
 |-  ( ( i e. _om /\ ( i u. j ) e. _om /\ i C_ ( i u. j ) ) -> ( L ` i ) C_ ( L ` ( i u. j ) ) )
58 56 57 mp3an3 
 |-  ( ( i e. _om /\ ( i u. j ) e. _om ) -> ( L ` i ) C_ ( L ` ( i u. j ) ) )
59 55 58 syldan 
 |-  ( ( i e. _om /\ j e. _om ) -> ( L ` i ) C_ ( L ` ( i u. j ) ) )
60 59 adantl 
 |-  ( ( ph /\ ( i e. _om /\ j e. _om ) ) -> ( L ` i ) C_ ( L ` ( i u. j ) ) )
61 60 sseld 
 |-  ( ( ph /\ ( i e. _om /\ j e. _om ) ) -> ( b e. ( L ` i ) -> b e. ( L ` ( i u. j ) ) ) )
62 simpr 
 |-  ( ( i e. _om /\ j e. _om ) -> j e. _om )
63 ssun2 
 |-  j C_ ( i u. j )
64 1 2 3 precsexlem7 
 |-  ( ( j e. _om /\ ( i u. j ) e. _om /\ j C_ ( i u. j ) ) -> ( R ` j ) C_ ( R ` ( i u. j ) ) )
65 63 64 mp3an3 
 |-  ( ( j e. _om /\ ( i u. j ) e. _om ) -> ( R ` j ) C_ ( R ` ( i u. j ) ) )
66 62 55 65 syl2anc 
 |-  ( ( i e. _om /\ j e. _om ) -> ( R ` j ) C_ ( R ` ( i u. j ) ) )
67 66 sseld 
 |-  ( ( i e. _om /\ j e. _om ) -> ( c e. ( R ` j ) -> c e. ( R ` ( i u. j ) ) ) )
68 67 adantl 
 |-  ( ( ph /\ ( i e. _om /\ j e. _om ) ) -> ( c e. ( R ` j ) -> c e. ( R ` ( i u. j ) ) ) )
69 4 ad2antrr 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) ) -> A e. No )
70 1 2 3 4 5 6 precsexlem8 
 |-  ( ( ph /\ ( i u. j ) e. _om ) -> ( ( L ` ( i u. j ) ) C_ No /\ ( R ` ( i u. j ) ) C_ No ) )
71 70 simpld 
 |-  ( ( ph /\ ( i u. j ) e. _om ) -> ( L ` ( i u. j ) ) C_ No )
72 71 sselda 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ b e. ( L ` ( i u. j ) ) ) -> b e. No )
73 72 adantrr 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) ) -> b e. No )
74 69 73 mulscld 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) ) -> ( A x.s b ) e. No )
75 70 simprd 
 |-  ( ( ph /\ ( i u. j ) e. _om ) -> ( R ` ( i u. j ) ) C_ No )
76 75 sselda 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ c e. ( R ` ( i u. j ) ) ) -> c e. No )
77 76 adantrl 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) ) -> c e. No )
78 69 77 mulscld 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) ) -> ( A x.s c ) e. No )
79 74 78 jca 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) ) -> ( ( A x.s b ) e. No /\ ( A x.s c ) e. No ) )
80 1 2 3 4 5 6 precsexlem9 
 |-  ( ( ph /\ ( i u. j ) e. _om ) -> ( A. b e. ( L ` ( i u. j ) ) ( A x.s b )
81 80 simpld 
 |-  ( ( ph /\ ( i u. j ) e. _om ) -> A. b e. ( L ` ( i u. j ) ) ( A x.s b )
82 rsp 
 |-  ( A. b e. ( L ` ( i u. j ) ) ( A x.s b )  ( b e. ( L ` ( i u. j ) ) -> ( A x.s b )
83 81 82 syl 
 |-  ( ( ph /\ ( i u. j ) e. _om ) -> ( b e. ( L ` ( i u. j ) ) -> ( A x.s b )
84 80 simprd 
 |-  ( ( ph /\ ( i u. j ) e. _om ) -> A. c e. ( R ` ( i u. j ) ) 1s
85 rsp 
 |-  ( A. c e. ( R ` ( i u. j ) ) 1s  ( c e. ( R ` ( i u. j ) ) -> 1s
86 84 85 syl 
 |-  ( ( ph /\ ( i u. j ) e. _om ) -> ( c e. ( R ` ( i u. j ) ) -> 1s
87 83 86 anim12d 
 |-  ( ( ph /\ ( i u. j ) e. _om ) -> ( ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) -> ( ( A x.s b )
88 87 imp 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) ) -> ( ( A x.s b )
89 1sno 
 |-  1s e. No
90 slttr 
 |-  ( ( ( A x.s b ) e. No /\ 1s e. No /\ ( A x.s c ) e. No ) -> ( ( ( A x.s b )  ( A x.s b )
91 89 90 mp3an2 
 |-  ( ( ( A x.s b ) e. No /\ ( A x.s c ) e. No ) -> ( ( ( A x.s b )  ( A x.s b )
92 79 88 91 sylc 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) ) -> ( A x.s b )
93 5 ad2antrr 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) ) -> 0s
94 73 77 69 93 sltmul2d 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) ) -> ( b  ( A x.s b )
95 92 94 mpbird 
 |-  ( ( ( ph /\ ( i u. j ) e. _om ) /\ ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) ) -> b
96 95 ex 
 |-  ( ( ph /\ ( i u. j ) e. _om ) -> ( ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) -> b
97 55 96 sylan2 
 |-  ( ( ph /\ ( i e. _om /\ j e. _om ) ) -> ( ( b e. ( L ` ( i u. j ) ) /\ c e. ( R ` ( i u. j ) ) ) -> b
98 61 68 97 syl2and 
 |-  ( ( ph /\ ( i e. _om /\ j e. _om ) ) -> ( ( b e. ( L ` i ) /\ c e. ( R ` j ) ) -> b
99 98 rexlimdvva 
 |-  ( ph -> ( E. i e. _om E. j e. _om ( b e. ( L ` i ) /\ c e. ( R ` j ) ) -> b
100 54 99 biimtrid 
 |-  ( ph -> ( ( b e. U. ( L " _om ) /\ c e. U. ( R " _om ) ) -> b
101 100 3impib 
 |-  ( ( ph /\ b e. U. ( L " _om ) /\ c e. U. ( R " _om ) ) -> b
102 21 32 38 43 101 ssltd 
 |-  ( ph -> U. ( L " _om ) <