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

Theorem nobnddown 25569
 Description: Any set of surreals is bounded below by a surreal with a birthday no greater than the successor of their maximum birthday. (Contributed by Scott Fenton, 10-Apr-2017.)
Assertion
Ref Expression
nobnddown
Distinct variable group:   ,,
Allowed substitution hints:   (,)

Proof of Theorem nobnddown
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2924 . 2
2 1on 6690 . . . . . . 7
32elexi 2925 . . . . . 6
43prid1 3872 . . . . 5
5 eqid 2404 . . . . 5
64, 5nobndlem2 25561 . . . 4
7 noxp1o 25534 . . . 4
86, 7syl 16 . . 3
98adantr 452 . . . . 5
10 ssel2 3303 . . . . . 6
1110adantlr 696 . . . . 5
124nobndlem4 25563 . . . . . . . 8
1310, 12syl 16 . . . . . . 7
1413adantlr 696 . . . . . 6
156adantr 452 . . . . . . . . . . 11
164, 5nobndlem6 25565 . . . . . . . . . . . 12
1716adantlr 696 . . . . . . . . . . 11
18 onelss 4583 . . . . . . . . . . 11
1915, 17, 18sylc 58 . . . . . . . . . 10
2019sselda 3308 . . . . . . . . 9
213fvconst2 5906 . . . . . . . . 9
2220, 21syl 16 . . . . . . . 8
2314adantr 452 . . . . . . . . . . . . . . . 16
24 onss 4730 . . . . . . . . . . . . . . . . . 18
2514, 24syl 16 . . . . . . . . . . . . . . . . 17
2625sselda 3308 . . . . . . . . . . . . . . . 16
27 ontri1 4575 . . . . . . . . . . . . . . . 16
2823, 26, 27syl2anc 643 . . . . . . . . . . . . . . 15
2928biimpd 199 . . . . . . . . . . . . . 14
3029con2d 109 . . . . . . . . . . . . 13
3130ex 424 . . . . . . . . . . . 12
3231pm2.43d 46 . . . . . . . . . . 11
3332imp 419 . . . . . . . . . 10
34 intss1 4025 . . . . . . . . . 10
3533, 34nsyl 115 . . . . . . . . 9
36 df-ne 2569 . . . . . . . . . 10
37 fveq2 5687 . . . . . . . . . . . . . 14
3837neeq1d 2580 . . . . . . . . . . . . 13
3938elrab3 3053 . . . . . . . . . . . 12
4039biimprd 215 . . . . . . . . . . 11
4126, 40syl 16 . . . . . . . . . 10
4236, 41syl5bir 210 . . . . . . . . 9
4335, 42mt3d 119 . . . . . . . 8
4422, 43eqtr4d 2439 . . . . . . 7
4544ralrimiva 2749 . . . . . 6
463fvconst2 5906 . . . . . . . 8
4717, 46syl 16 . . . . . . 7
484nobndlem5 25564 . . . . . . . . . . . . . 14
4911, 48syl 16 . . . . . . . . . . . . 13
5049neneqd 2583 . . . . . . . . . . . 12
51 nofv 25525 . . . . . . . . . . . . 13
5211, 51syl 16 . . . . . . . . . . . 12
53 3orel2 25118 . . . . . . . . . . . 12
5450, 52, 53sylc 58 . . . . . . . . . . 11
55 eqid 2404 . . . . . . . . . . 11
5654, 55jctil 524 . . . . . . . . . 10
5756ex-natded9.20 21678 . . . . . . . . 9
5857orcd 382 . . . . . . . 8
59 fvex 5701 . . . . . . . . . 10
603, 59brtp 25320 . . . . . . . . 9
61 df-3or 937 . . . . . . . . 9
6260, 61bitri 241 . . . . . . . 8
6358, 62sylibr 204 . . . . . . 7
6447, 63eqbrtrd 4192 . . . . . 6
65 raleq 2864 . . . . . . . 8
66 fveq2 5687 . . . . . . . . 9
67 fveq2 5687 . . . . . . . . 9
6866, 67breq12d 4185 . . . . . . . 8
6965, 68anbi12d 692 . . . . . . 7
7069rspcev 3012 . . . . . 6
7114, 45, 64, 70syl12anc 1182 . . . . 5
72 sltval 25515 . . . . . 6
7372biimpar 472 . . . . 5
749, 11, 71, 73syl21anc 1183 . . . 4
7574ralrimiva 2749 . . 3
764, 5nobndlem8 25567 . . 3
77 breq1 4175 . . . . . 6
7877ralbidv 2686 . . . . 5
79 fveq2 5687 . . . . . 6
8079sseq1d 3335 . . . . 5
8178, 80anbi12d 692 . . . 4
8281rspcev 3012 . . 3
838, 75, 76, 82syl12anc 1182 . 2
841, 83sylan2 461 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   w3o 935   wceq 1649   wcel 1721   wne 2567  wral 2666  wrex 2667  crab 2670  cvv 2916   wss 3280  c0 3588  csn 3774  ctp 3776  cop 3777  cuni 3975  cint 4010   class class class wbr 4172  con0 4541   csuc 4543   cxp 4835  cima 4840  cfv 5413  c1o 6676  c2o 6677  csur 25508  cslt 25509  cbday 25510 This theorem is referenced by:  nofulllem2  25571 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-suc 4547  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-1o 6683  df-2o 6684  df-no 25511  df-slt 25512  df-bday 25513
 Copyright terms: Public domain W3C validator