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

Theorem nodense 25557
 Description: Given two distinct surreals with the same birthday, there is an older surreal lying between the two of them. Alling's axiom (SD) (Contributed by Scott Fenton, 16-Jun-2011.)
Assertion
Ref Expression
nodense
Distinct variable groups:   ,   ,

Proof of Theorem nodense
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nodenselem6 25554 . 2
2 bdayval 25516 . . . . 5
31, 2syl 16 . . . 4
4 dmres 5126 . . . . 5
5 nodenselem5 25553 . . . . . . . 8
6 bdayelon 25548 . . . . . . . . 9
76onelssi 4649 . . . . . . . 8
85, 7syl 16 . . . . . . 7
9 bdayval 25516 . . . . . . . 8
109ad2antrr 707 . . . . . . 7
118, 10sseqtrd 3344 . . . . . 6
12 df-ss 3294 . . . . . 6
1311, 12sylib 189 . . . . 5
144, 13syl5eq 2448 . . . 4
153, 14eqtrd 2436 . . 3
1615, 5eqeltrd 2478 . 2
17 nodenselem4 25552 . . . . 5
1817adantrl 697 . . . 4
19 nodenselem8 25556 . . . . . . . . . . . . 13
2019biimpd 199 . . . . . . . . . . . 12
21203expia 1155 . . . . . . . . . . 11
2221imp32 423 . . . . . . . . . 10
2322simpld 446 . . . . . . . . 9
24 eqid 2404 . . . . . . . . 9
2523, 24jctir 525 . . . . . . . 8
26253mix1d 25123 . . . . . . 7
27 fvex 5701 . . . . . . . 8
28 0ex 4299 . . . . . . . 8
2927, 28brtp 25320 . . . . . . 7
3026, 29sylibr 204 . . . . . 6
3115fveq2d 5691 . . . . . . 7
32 fvnobday 25550 . . . . . . . 8
331, 32syl 16 . . . . . . 7
3431, 33eqtr3d 2438 . . . . . 6
3530, 34breqtrrd 4198 . . . . 5
36 fvres 5704 . . . . . . 7
3736eqcomd 2409 . . . . . 6
3837rgen 2731 . . . . 5
3935, 38jctil 524 . . . 4
40 raleq 2864 . . . . . 6
41 fveq2 5687 . . . . . . 7
42 fveq2 5687 . . . . . . 7
4341, 42breq12d 4185 . . . . . 6
4440, 43anbi12d 692 . . . . 5
4544rspcev 3012 . . . 4
4618, 39, 45syl2anc 643 . . 3
47 simpll 731 . . . 4
48 sltval 25515 . . . 4
4947, 1, 48syl2anc 643 . . 3
5046, 49mpbird 224 . 2
5137adantl 453 . . . . . 6
52 nodenselem7 25555 . . . . . . 7
5352imp 419 . . . . . 6
5451, 53eqtr3d 2438 . . . . 5
5554ralrimiva 2749 . . . 4
5622simprd 450 . . . . . . . 8
5756, 24jctil 524 . . . . . . 7
58573mix3d 25125 . . . . . 6
59 fvex 5701 . . . . . . 7
6028, 59brtp 25320 . . . . . 6
6158, 60sylibr 204 . . . . 5
6234, 61eqbrtrd 4192 . . . 4
63 raleq 2864 . . . . . 6
64 fveq2 5687 . . . . . . 7
6542, 64breq12d 4185 . . . . . 6
6663, 65anbi12d 692 . . . . 5
6766rspcev 3012 . . . 4
6818, 55, 62, 67syl12anc 1182 . . 3
69 simplr 732 . . . 4
70 sltval 25515 . . . 4
711, 69, 70syl2anc 643 . . 3
7268, 71mpbird 224 . 2
73 fveq2 5687 . . . . 5
7473eleq1d 2470 . . . 4
75 breq2 4176 . . . 4
76 breq1 4175 . . . 4
7774, 75, 763anbi123d 1254 . . 3
7877rspcev 3012 . 2
791, 16, 50, 72, 78syl13anc 1186 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3o 935   w3a 936   wceq 1649   wcel 1721   wne 2567  wral 2666  wrex 2667  crab 2670   cin 3279   wss 3280  c0 3588  ctp 3776  cop 3777  cint 4010   class class class wbr 4172  con0 4541   cdm 4837   cres 4839  cfv 5413  c1o 6676  c2o 6677  csur 25508  cslt 25509  cbday 25510 This theorem is referenced by:  nocvxminlem  25558 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