Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nofulllem5 Structured version   Unicode version

Theorem nofulllem5 25661
 Description: Lemma for nofull (future) . Here, we introduce a new surreal number . Eventually, we will show that either or a related surreal number has the required properties for the final theorem. We begin by calculating the domain of . (Contributed by Scott Fenton, 1-May-2017.)
Hypotheses
Ref Expression
nofulllem5.1
nofulllem5.2
nofulllem5.3
Assertion
Ref Expression
nofulllem5
Distinct variable groups:   ,,,,,,   ,,,,,,   ,,,,,,   ,,,,,,   ,,,,
Allowed substitution hints:   (,,,,,)   (,)   (,,,,,)

Proof of Theorem nofulllem5
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nofulllem5.3 . . . 4
21dmeqi 5071 . . 3
3 dmuni 5079 . . 3
42, 3eqtri 2456 . 2
5 iunss 4132 . . . . 5
6 vex 2959 . . . . . . 7
7 eqeq2 2445 . . . . . . . . . 10
8 eqeq2 2445 . . . . . . . . . 10
97, 8anbi12d 692 . . . . . . . . 9
109rexbidv 2726 . . . . . . . 8
11102rexbidv 2748 . . . . . . 7
12 nofulllem5.2 . . . . . . 7
136, 11, 12elab2 3085 . . . . . 6
14 inss1 3561 . . . . . . . . . . . 12
15 elssuni 4043 . . . . . . . . . . . 12
1614, 15syl5ss 3359 . . . . . . . . . . 11
17 dmres 5167 . . . . . . . . . . . . 13
18 dmeq 5070 . . . . . . . . . . . . 13
1917, 18syl5eqr 2482 . . . . . . . . . . . 12
2019sseq1d 3375 . . . . . . . . . . 11
2116, 20syl5ibcom 212 . . . . . . . . . 10
2221adantrd 455 . . . . . . . . 9
2322rexlimiv 2824 . . . . . . . 8
2423a1i 11 . . . . . . 7
2524rexlimivv 2835 . . . . . 6
2613, 25sylbi 188 . . . . 5
275, 26mprgbir 2776 . . . 4
2827a1i 11 . . 3
29 nofulllem5.1 . . . . . . . . 9
3029nofulllem4 25660 . . . . . . . 8
31 eloni 4591 . . . . . . . 8
3230, 31syl 16 . . . . . . 7
33 ordsucuniel 4804 . . . . . . 7
3432, 33syl 16 . . . . . 6
35 simpr 448 . . . . . . . 8
36 onss 4771 . . . . . . . . . . . . 13
3730, 36syl 16 . . . . . . . . . . . 12
3837sselda 3348 . . . . . . . . . . 11
39 ssrab2 3428 . . . . . . . . . . . . . . . . . . 19
40 onnmin 4783 . . . . . . . . . . . . . . . . . . 19
4139, 40mpan 652 . . . . . . . . . . . . . . . . . 18
4241adantl 453 . . . . . . . . . . . . . . . . 17
4329eleq2i 2500 . . . . . . . . . . . . . . . . 17
4442, 43sylnibr 297 . . . . . . . . . . . . . . . 16
4544ex 424 . . . . . . . . . . . . . . 15
4645con2d 109 . . . . . . . . . . . . . 14
4746imp 419 . . . . . . . . . . . . 13
48 reseq2 5141 . . . . . . . . . . . . . . . . 17
49 reseq2 5141 . . . . . . . . . . . . . . . . 17
5048, 49neeq12d 2616 . . . . . . . . . . . . . . . 16
51502ralbidv 2747 . . . . . . . . . . . . . . 15
52 reseq1 5140 . . . . . . . . . . . . . . . . 17
5352neeq1d 2614 . . . . . . . . . . . . . . . 16
54 reseq1 5140 . . . . . . . . . . . . . . . . 17
5554neeq2d 2615 . . . . . . . . . . . . . . . 16
5653, 55cbvral2v 2940 . . . . . . . . . . . . . . 15
5751, 56syl6bb 253 . . . . . . . . . . . . . 14
5857elrab 3092 . . . . . . . . . . . . 13
5947, 58sylnib 296 . . . . . . . . . . . 12
60 imnan 412 . . . . . . . . . . . 12
6159, 60sylibr 204 . . . . . . . . . . 11
6238, 61mpd 15 . . . . . . . . . 10
63 df-ne 2601 . . . . . . . . . . . . . . 15
6463con2bii 323 . . . . . . . . . . . . . 14
6564rexbii 2730 . . . . . . . . . . . . 13
66 rexnal 2716 . . . . . . . . . . . . 13
6765, 66bitri 241 . . . . . . . . . . . 12
6867rexbii 2730 . . . . . . . . . . 11
69 rexnal 2716 . . . . . . . . . . 11
7068, 69bitri 241 . . . . . . . . . 10
7162, 70sylibr 204 . . . . . . . . 9
72 simp3 959 . . . . . . . . . . . . . . . . . . . 20
73 breq1 4215 . . . . . . . . . . . . . . . . . . . . 21
74 breq2 4216 . . . . . . . . . . . . . . . . . . . . 21
7573, 74rspc2v 3058 . . . . . . . . . . . . . . . . . . . 20
7672, 75mpan9 456 . . . . . . . . . . . . . . . . . . 19
7776adantrl 697 . . . . . . . . . . . . . . . . . 18
78 simp1l 981 . . . . . . . . . . . . . . . . . . . 20
79 simprl 733 . . . . . . . . . . . . . . . . . . . 20
80 ssel2 3343 . . . . . . . . . . . . . . . . . . . 20
8178, 79, 80syl2an 464 . . . . . . . . . . . . . . . . . . 19
82 sltirr 25625 . . . . . . . . . . . . . . . . . . 19
8381, 82syl 16 . . . . . . . . . . . . . . . . . 18
84 breq2 4216 . . . . . . . . . . . . . . . . . . . 20
8584biimprcd 217 . . . . . . . . . . . . . . . . . . 19
8685con3d 127 . . . . . . . . . . . . . . . . . 18
8777, 83, 86sylc 58 . . . . . . . . . . . . . . . . 17
8887adantr 452 . . . . . . . . . . . . . . . 16
89 ioran 477 . . . . . . . . . . . . . . . . 17
90 simp2l 983 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
91 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
92 ssel2 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9390, 91, 92syl2an 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9493adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
95 nofun 25604 . . . . . . . . . . . . . . . . . . . . . . . . 25
96 funrel 5471 . . . . . . . . . . . . . . . . . . . . . . . . 25
9794, 95, 963syl 19 . . . . . . . . . . . . . . . . . . . . . . . 24
9832adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
99 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
100 ordelon 4605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
10198, 99, 100syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102 sucelon 4797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
103101, 102sylibr 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
104 eloni 4591 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105103, 104syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
106 nodmord 25608 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10793, 106syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
108 ordtri2or 4677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
109105, 107, 108syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26
110109orcanai 880 . . . . . . . . . . . . . . . . . . . . . . . . 25
111 sssucid 4658 . . . . . . . . . . . . . . . . . . . . . . . . 25
112110, 111syl6ss 3360 . . . . . . . . . . . . . . . . . . . . . . . 24
113 relssres 5183 . . . . . . . . . . . . . . . . . . . . . . . 24
11497, 112, 113syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
115114ex 424 . . . . . . . . . . . . . . . . . . . . . 22
11681adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
117 nofun 25604 . . . . . . . . . . . . . . . . . . . . . . . . 25
118 funrel 5471 . . . . . . . . . . . . . . . . . . . . . . . . 25
119116, 117, 1183syl 19 . . . . . . . . . . . . . . . . . . . . . . . 24
120 nodmord 25608 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
12181, 120syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
122 ordtri2or 4677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
123105, 121, 122syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26
124123orcanai 880 . . . . . . . . . . . . . . . . . . . . . . . . 25
125124, 111syl6ss 3360 . . . . . . . . . . . . . . . . . . . . . . . 24
126 relssres 5183 . . . . . . . . . . . . . . . . . . . . . . . 24
127119, 125, 126syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
128127ex 424 . . . . . . . . . . . . . . . . . . . . . 22
129115, 128anim12d 547 . . . . . . . . . . . . . . . . . . . . 21
130129ancomsd 441 . . . . . . . . . . . . . . . . . . . 20
131 eqeq12 2448 . . . . . . . . . . . . . . . . . . . . . 22
132131biimpd 199 . . . . . . . . . . . . . . . . . . . . 21
133132ancoms 440 . . . . . . . . . . . . . . . . . . . 20
134130, 133syl6 31 . . . . . . . . . . . . . . . . . . 19
135134com23 74 . . . . . . . . . . . . . . . . . 18
136135imp 419 . . . . . . . . . . . . . . . . 17
13789, 136syl5bi 209 . . . . . . . . . . . . . . . 16
13888, 137mt3d 119 . . . . . . . . . . . . . . 15
139138ex 424 . . . . . . . . . . . . . 14
140139anassrs 630 . . . . . . . . . . . . 13
141140anassrs 630 . . . . . . . . . . . 12
142141ancld 537 . . . . . . . . . . 11
143142reximdva 2818 . . . . . . . . . 10
144143reximdva 2818 . . . . . . . . 9
14571, 144mpd 15 . . . . . . . 8
146 reseq2 5141 . . . . . . . . . . . . 13
147 reseq2 5141 . . . . . . . . . . . . 13
148146, 147eqeq12d 2450 . . . . . . . . . . . 12
149 eleq2 2497 . . . . . . . . . . . 12
150148, 1493anbi13d 1256 . . . . . . . . . . 11
151 vex 2959 . . . . . . . . . . . . 13
152151sucid 4660 . . . . . . . . . . . 12
153 df-3an 938 . . . . . . . . . . . 12
154152, 153mpbiran2 886 . . . . . . . . . . 11
155150, 154syl6bb 253 . . . . . . . . . 10
1561552rexbidv 2748 . . . . . . . . 9
157156rspcev 3052 . . . . . . . 8
15835, 145, 157syl2anc 643 . . . . . . 7
159158ex 424 . . . . . 6
16034, 159sylbid 207 . . . . 5
161 eliun 4097 . . . . . 6
16212rexeqi 2909 . . . . . 6
163 r19.41v 2861 . . . . . . . . . . . 12
164163rexbii 2730 . . . . . . . . . . 11
165 r19.41v 2861 . . . . . . . . . . 11
166164, 165bitri 241 . . . . . . . . . 10
167166rexbii 2730 . . . . . . . . 9
168 r19.41v 2861 . . . . . . . . 9
169167, 168bitri 241 . . . . . . . 8
170169exbii 1592 . . . . . . 7
171 rexcom 2869 . . . . . . . . 9
172 rexcom 2869 . . . . . . . . . 10
173172rexbii 2730 . . . . . . . . 9
174171, 173bitri 241 . . . . . . . 8
175 vex 2959 . . . . . . . . . . . . . . . 16
176175resex 5186 . . . . . . . . . . . . . . 15
177 eqeq2 2445 . . . . . . . . . . . . . . . 16
178 dmeq 5070 . . . . . . . . . . . . . . . . 17
179178eleq2d 2503 . . . . . . . . . . . . . . . 16
180177, 179anbi12d 692 . . . . . . . . . . . . . . 15
181176, 180ceqsexv 2991 . . . . . . . . . . . . . 14
182 an12 773 . . . . . . . . . . . . . . . 16
183 eqcom 2438 . . . . . . . . . . . . . . . . 17
184183anbi1i 677 . . . . . . . . . . . . . . . 16
185 anass 631 . . . . . . . . . . . . . . . 16
186182, 184, 1853bitr4i 269 . . . . . . . . . . . . . . 15
187186exbii 1592 . . . . . . . . . . . . . 14
188 dmeq 5070 . . . . . . . . . . . . . . . . . . . 20
189188eleq2d 2503 . . . . . . . . . . . . . . . . . . 19
190189orbi1d 684 . . . . . . . . . . . . . . . . . 18
191 oridm 501 . . . . . . . . . . . . . . . . . 18
192190, 191syl6rbb 254 . . . . . . . . . . . . . . . . 17
193 incom 3533 . . . . . . . . . . . . . . . . . . . . 21
19417, 193eqtri 2456 . . . . . . . . . . . . . . . . . . . 20
195194elin2 3531 . . . . . . . . . . . . . . . . . . 19
196 dmres 5167 . . . . . . . . . . . . . . . . . . . . 21
197 incom 3533 . . . . . . . . . . . . . . . . . . . . 21
198196, 197eqtri 2456 . . . . . . . . . . . . . . . . . . . 20
199198elin2 3531 . . . . . . . . . . . . . . . . . . 19
200195, 199orbi12i 508 . . . . . . . . . . . . . . . . . 18
201 andir 839 . . . . . . . . . . . . . . . . . 18
202200, 201bitr4i 244 . . . . . . . . . . . . . . . . 17
203192, 202syl6bb 253 . . . . . . . . . . . . . . . 16
204203pm5.32i 619 . . . . . . . . . . . . . . 15
205 3anass 940 . . . . . . . . . . . . . . 15
206204, 205bitr4i 244 . . . . . . . . . . . . . 14
207181, 187, 2063bitr3ri 268 . . . . . . . . . . . . 13
208207rexbii 2730 . . . . . . . . . . . 12
209 rexcom4 2975 . . . . . . . . . . . 12
210208, 209bitri 241 . . . . . . . . . . 11
211210rexbii 2730 . . . . . . . . . 10
212 rexcom4 2975 . . . . . . . . . 10
213211, 212bitri 241 . . . . . . . . 9
214213rexbii 2730 . . . . . . . 8
215 rexcom4 2975 . . . . . . . 8
216174, 214, 2153bitri 263 . . . . . . 7
21711rexab 3097 . . . . . . 7
218170, 216, 2173bitr4ri 270 . . . . . 6
219161, 162, 2183bitri 263 . . . . 5
220160, 219syl6ibr 219 . . . 4
221220ssrdv 3354 . . 3
22228, 221eqssd 3365 . 2
2234, 222syl5eq 2480 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   w3a 936  wex 1550   wceq 1652   wcel 1725  cab 2422   wne 2599  wral 2705  wrex 2706  crab 2709   cin 3319   wss 3320  cuni 4015  cint 4050  ciun 4093   class class class wbr 4212   word 4580  con0 4581   csuc 4583   cdm 4878   cres 4880   wrel 4883   wfun 5448  csur 25595  cslt 25596 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-uni 4016  df-int 4051  df-iun 4095  df-br 4213  df-opab 4267  df-mpt 4268  df-tr 4303  df-eprel 4494  df-id 4498  df-po 4503  df-so 4504  df-fr 4541  df-we 4543  df-ord 4584  df-on 4585  df-suc 4587  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-1o 6724  df-2o 6725  df-no 25598  df-slt 25599  df-bday 25600
 Copyright terms: Public domain W3C validator