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

Theorem supsr 7167
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 2911 . . 3
2 vex 2327 . . . . . . . . . . . . 13
3 ltrelsr 7126 . . . . . . . . . . . . 13
42, 3brel 4070 . . . . . . . . . . . 12
54simpld 438 . . . . . . . . . . 11
65ralimi 2193 . . . . . . . . . 10
7 dfss3 2649 . . . . . . . . . 10
86, 7sylibr 201 . . . . . . . . 9
98sseld 2658 . . . . . . . 8
109rexlimivw 2238 . . . . . . 7
1110impcom 415 . . . . . 6
12 eleq1 1977 . . . . . . . . 9
1312anbi1d 679 . . . . . . . 8
1413imbi1d 306 . . . . . . 7
15 opeq1 3201 . . . . . . . . . . . 12
16 eceq1 5673 . . . . . . . . . . . 12
1715, 16syl 15 . . . . . . . . . . 11
1817oveq2d 4992 . . . . . . . . . 10
1918eleq1d 1983 . . . . . . . . 9
2019cbvabv 2454 . . . . . . . 8
21 1sr 7136 . . . . . . . . 9
2221elimel 3058 . . . . . . . 8
2320, 22supsrlem 7166 . . . . . . 7
2414, 23dedth 3047 . . . . . 6
2511, 24mpcom 32 . . . . 5
2625ex 419 . . . 4
2726exlimiv 1718 . . 3
281, 27sylbi 185 . 2
2928imp 414 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 357  wex 1335   wceq 1414   wcel 1416  cab 1905   wne 2035  wral 2127  wrex 2128   wss 2634  c0 2902  cif 3008  cop 3082   class class class wbr 3370  (class class class)co 4979  cec 5641  c1p 6913   cer 6919  cnr 6920  c1r 6922   cplr 6924   cltr 6926
This theorem is referenced by:  axpre-sup 7223
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-13 1422  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-rep 3456  ax-sep 3466  ax-nul 3475  ax-pow 3511  ax-pr 3535  ax-un 3809  ax-inf2 6217
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1309  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-ral 2131  df-rex 2132  df-reu 2133  df-rab 2134  df-v 2326  df-sbc 2493  df-csb 2575  df-dif 2637  df-un 2639  df-in 2641  df-ss 2645  df-pss 2647  df-nul 2903  df-if 3009  df-pw 3068  df-sn 3085  df-pr 3086  df-tp 3087  df-op 3088  df-uni 3224  df-int 3258  df-iun 3297  df-br 3371  df-opab 3425  df-tr 3440  df-eprel 3620  df-id 3623  df-po 3628  df-so 3642  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-lim 3696  df-suc 3697  df-om 3974  df-xp 4021  df-rel 4022  df-cnv 4023  df-co 4024  df-dm 4025  df-rn 4026  df-res 4027  df-ima 4028  df-fun 4029  df-fn 4030  df-f 4031  df-fv 4035  df-ov 4981  df-oprab 4982  df-mpt 5142  df-mpt2 5143  df-1st 5269  df-2nd 5270  df-rdg 5468  df-1o 5505  df-oadd 5509  df-omul 5510  df-er 5643  df-ec 5645  df-qs 5649  df-ni 6927  df-pli 6928  df-mi 6929  df-lti 6930  df-plpq 6963  df-mpq 6964  df-ltpq 6965  df-enq 6966  df-nq 6967  df-erq 6968  df-plq 6969  df-mq 6970  df-1nq 6971  df-rq 6972  df-ltnq 6973  df-np 7037  df-1p 7038  df-plp 7039  df-mp 7040  df-ltp 7041  df-plpr 7111  df-mpr 7112  df-enr 7113  df-nr 7114  df-plr 7115  df-mr 7116  df-ltr 7117  df-0r 7118  df-1r 7119  df-m1r 7120
Copyright terms: Public domain