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