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 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 ∘ F
precsexlem.3 ⊢ R = 2 nd ∘ F
precsexlem.4 ⊢ φ → A ∈ No
precsexlem.5 ⊢ φ → 0 s < s A
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 ⊢ φ → ⋃ L ω ≪ s ⋃ R ω

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