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

Theorem supsr 7169
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 7128 . . . . . . . . . . . . 13
42, 3brel 4072 . . . . . . . . . . . 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 3203 . . . . . . . . . . . 12
16 eceq1 5675 . . . . . . . . . . . 12
1715, 16syl 15 . . . . . . . . . . 11
1817oveq2d 4994 . . . . . . . . . 10
1918eleq1d 1983 . . . . . . . . 9
2019cbvabv 2454 . . . . . . . 8
21 1sr 7138 . . . . . . . . 9
2221elimel 3059 . . . . . . . 8
2320, 22supsrlem 7168 . . . . . . 7
2414, 23dedth 3048 . . . . . 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 3083   class class class wbr 3372  (class class class)co 4981  cec 5643  c1p 6915   cer 6921  cnr 6922  c1r 6924   cplr 6926   cltr 6928
This theorem is referenced by:  axpre-sup 7225
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 3458  ax-sep 3468  ax-nul 3477  ax-pow 3513  ax-pr 3537  ax-un 3811  ax-inf2 6219
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 3069  df-sn 3086  df-pr 3087  df-tp 3088  df-op 3089  df-uni 3226  df-int 3260  df-iun 3299  df-br 3373  df-opab 3427  df-tr 3442  df-eprel 3622  df-id 3625  df-po 3630  df-so 3644  df-fr 3664  df-we 3680  df-ord 3696  df-on 3697  df-lim 3698  df-suc 3699  df-om 3976  df-xp 4023  df-rel 4024  df-cnv 4025  df-co 4026  df-dm 4027  df-rn 4028  df-res 4029  df-ima 4030  df-fun 4031  df-fn 4032  df-f 4033  df-fv 4037  df-ov 4983  df-oprab 4984  df-mpt 5144  df-mpt2 5145  df-1st 5271  df-2nd 5272  df-rdg 5470  df-1o 5507  df-oadd 5511  df-omul 5512  df-er 5645  df-ec 5647  df-qs 5651  df-ni 6929  df-pli 6930  df-mi 6931  df-lti 6932  df-plpq 6965  df-mpq 6966  df-ltpq 6967  df-enq 6968  df-nq 6969  df-erq 6970  df-plq 6971  df-mq 6972  df-1nq 6973  df-rq 6974  df-ltnq 6975  df-np 7039  df-1p 7040  df-plp 7041  df-mp 7042  df-ltp 7043  df-plpr 7113  df-mpr 7114  df-enr 7115  df-nr 7116  df-plr 7117  df-mr 7118  df-ltr 7119  df-0r 7120  df-1r 7121  df-m1r 7122
Copyright terms: Public domain