HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem supsr 7905
Description: A non-empty, bounded set of signed reals has a supremum. (Cotributed by Mario Carneiro, 15-Jun-2013.)
Assertion
Ref Expression
supsr
Distinct variable group:   ,,,

Proof of Theorem supsr
StepHypRef Expression
1 n0 3034 . . 3
2 ltrelsr 7864 . . . . . . . . . . . . 13
32brel 4236 . . . . . . . . . . . 12
43simpld 438 . . . . . . . . . . 11
54ralimi 2305 . . . . . . . . . 10
6 dfss3 2765 . . . . . . . . . 10
75, 6sylibr 201 . . . . . . . . 9
87sseld 2774 . . . . . . . 8
98rexlimivw 2350 . . . . . . 7
109impcom 415 . . . . . 6
11 eleq1 2089 . . . . . . . . 9
1211anbi1d 679 . . . . . . . 8
1312imbi1d 306 . . . . . . 7
14 opeq1 3348 . . . . . . . . . . . 12
15 eceq1 5982 . . . . . . . . . . . 12
1614, 15syl 15 . . . . . . . . . . 11
1716oveq2d 5219 . . . . . . . . . 10
1817eleq1d 2095 . . . . . . . . 9
1918cbvabv 2570 . . . . . . . 8
20 1sr 7874 . . . . . . . . 9
2120elimel 3186 . . . . . . . 8
2219, 21supsrlem 7904 . . . . . . 7
2313, 22dedth 3175 . . . . . 6
2410, 23mpcom 32 . . . . 5
2524ex 419 . . . 4
2625exlimiv 1830 . . 3
271, 26sylbi 185 . 2
2827imp 414 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 357  wex 1447   wceq 1526   wcel 1528  cab 2017   wne 2147  wral 2239  wrex 2240   wss 2750  c0 3025  cif 3134  cop 3211   class class class wbr 3531  (class class class)co 5206  cec 5950  c1p 7651   cer 7657  cnr 7658  c1r 7660   cplr 7662   cltr 7664
This theorem is referenced by:  axpre-sup 7961
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-13 1534  ax-14 1535  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-rep 3616  ax-sep 3626  ax-nul 3635  ax-pow 3671  ax-pr 3695  ax-un 3973  ax-inf2 6607
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1261  df-ex 1448  df-sb 1703  df-eu 1930  df-mo 1931  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-ral 2243  df-rex 2244  df-reu 2245  df-rab 2246  df-v 2442  df-sbc 2609  df-csb 2691  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-pss 2763  df-nul 3026  df-if 3135  df-pw 3196  df-sn 3214  df-pr 3215  df-tp 3216  df-op 3217  df-uni 3375  df-int 3409  df-iun 3451  df-br 3532  df-opab 3585  df-tr 3600  df-eprel 3783  df-id 3787  df-po 3792  df-so 3806  df-fr 3826  df-we 3842  df-ord 3858  df-on 3859  df-lim 3860  df-suc 3861  df-om 4139  df-xp 4186  df-rel 4187  df-cnv 4188  df-co 4189  df-dm 4190  df-rn 4191  df-res 4192  df-ima 4193  df-fun 4194  df-fn 4195  df-f 4196  df-fv 4200  df-ov 5208  df-oprab 5209  df-mpt 5371  df-mpt2 5372  df-1st 5521  df-2nd 5522  df-recs 5722  df-rdg 5750  df-1o 5798  df-oadd 5802  df-omul 5803  df-er 5952  df-ec 5954  df-qs 5958  df-ni 7665  df-pli 7666  df-mi 7667  df-lti 7668  df-plpq 7701  df-mpq 7702  df-ltpq 7703  df-enq 7704  df-nq 7705  df-erq 7706  df-plq 7707  df-mq 7708  df-1nq 7709  df-rq 7710  df-ltnq 7711  df-np 7775  df-1p 7776  df-plp 7777  df-mp 7778  df-ltp 7779  df-plpr 7849  df-mpr 7850  df-enr 7851  df-nr 7852  df-plr 7853  df-mr 7854  df-ltr 7855  df-0r 7856  df-1r 7857  df-m1r 7858
Copyright terms: Public domain