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

Theorem nobndup 25568
 Description: Any set of surreals is bounded above 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
nobndup
Distinct variable group:   ,,
Allowed substitution hints:   (,)

Proof of Theorem nobndup
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2on 6691 . . . . . 6
21elexi 2925 . . . . 5
32prid2 3873 . . . 4
4 eqid 2404 . . . 4
53, 4nobndlem2 25561 . . 3
6 noxp2o 25535 . . 3
75, 6syl 16 . 2
8 elex 2924 . . 3
9 ssel2 3303 . . . . . 6
109adantlr 696 . . . . 5
113, 4nobndlem2 25561 . . . . . . 7
1211, 6syl 16 . . . . . 6
1312adantr 452 . . . . 5
143nobndlem4 25563 . . . . . . 7
1510, 14syl 16 . . . . . 6
1615adantr 452 . . . . . . . . . . . . . . . 16
17 onelon 4566 . . . . . . . . . . . . . . . . 17
1815, 17sylan 458 . . . . . . . . . . . . . . . 16
19 ontri1 4575 . . . . . . . . . . . . . . . 16
2016, 18, 19syl2anc 643 . . . . . . . . . . . . . . 15
2120biimpd 199 . . . . . . . . . . . . . 14
2221con2d 109 . . . . . . . . . . . . 13
2322ex 424 . . . . . . . . . . . 12
2423pm2.43d 46 . . . . . . . . . . 11
2524imp 419 . . . . . . . . . 10
26 intss1 4025 . . . . . . . . . 10
2725, 26nsyl 115 . . . . . . . . 9
28 df-ne 2569 . . . . . . . . . 10
29 fveq2 5687 . . . . . . . . . . . . . 14
3029neeq1d 2580 . . . . . . . . . . . . 13
3130elrab3 3053 . . . . . . . . . . . 12
3231biimprd 215 . . . . . . . . . . 11
3318, 32syl 16 . . . . . . . . . 10
3428, 33syl5bir 210 . . . . . . . . 9
3527, 34mt3d 119 . . . . . . . 8
3611adantr 452 . . . . . . . . . . 11
373, 4nobndlem6 25565 . . . . . . . . . . . 12
3837adantlr 696 . . . . . . . . . . 11
39 onelss 4583 . . . . . . . . . . 11
4036, 38, 39sylc 58 . . . . . . . . . 10
4140sselda 3308 . . . . . . . . 9
422fvconst2 5906 . . . . . . . . 9
4341, 42syl 16 . . . . . . . 8
4435, 43eqtr4d 2439 . . . . . . 7
4544ralrimiva 2749 . . . . . 6
463nobndlem5 25564 . . . . . . . . . . . . . . . 16
4710, 46syl 16 . . . . . . . . . . . . . . 15
4847neneqd 2583 . . . . . . . . . . . . . 14
49 nofv 25525 . . . . . . . . . . . . . . 15
5010, 49syl 16 . . . . . . . . . . . . . 14
51 3orel3 25119 . . . . . . . . . . . . . 14
5248, 50, 51sylc 58 . . . . . . . . . . . . 13
5352orcomd 378 . . . . . . . . . . . 12
54 eqid 2404 . . . . . . . . . . . 12
5553, 54jctir 525 . . . . . . . . . . 11
56 andir 839 . . . . . . . . . . 11
5755, 56sylib 189 . . . . . . . . . 10
5857olcd 383 . . . . . . . . 9
59 3orass 939 . . . . . . . . 9
6058, 59sylibr 204 . . . . . . . 8
61 fvex 5701 . . . . . . . . 9
6261, 2brtp 25320 . . . . . . . 8
6360, 62sylibr 204 . . . . . . 7
643, 4nobndlem7 25566 . . . . . . . 8
6564adantlr 696 . . . . . . 7
6663, 65breqtrrd 4198 . . . . . 6
67 raleq 2864 . . . . . . . 8
68 fveq2 5687 . . . . . . . . 9
69 fveq2 5687 . . . . . . . . 9
7068, 69breq12d 4185 . . . . . . . 8
7167, 70anbi12d 692 . . . . . . 7
7271rspcev 3012 . . . . . 6
7315, 45, 66, 72syl12anc 1182 . . . . 5
74 sltval 25515 . . . . . 6
7574biimpar 472 . . . . 5
7610, 13, 73, 75syl21anc 1183 . . . 4
7776ralrimiva 2749 . . 3
788, 77sylan2 461 . 2
793, 4nobndlem8 25567 . 2
80 breq2 4176 . . . . 5
8180ralbidv 2686 . . . 4
82 fveq2 5687 . . . . 5
8382sseq1d 3335 . . . 4
8481, 83anbi12d 692 . . 3
8584rspcev 3012 . 2
867, 78, 79, 85syl12anc 1182 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:  nofulllem1  25570 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