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

Theorem supsr 7254
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 2916 . . 3
2 ltrelsr 7213 . . . . . . . . . . . . 13
32brel 4098 . . . . . . . . . . . 12
43simpld 438 . . . . . . . . . . 11
54ralimi 2193 . . . . . . . . . 10
6 dfss3 2652 . . . . . . . . . 10
75, 6sylibr 201 . . . . . . . . 9
87sseld 2661 . . . . . . . 8
98rexlimivw 2238 . . . . . . 7
109impcom 415 . . . . . 6
11 eleq1 1977 . . . . . . . . 9
1211anbi1d 679 . . . . . . . 8
1312imbi1d 306 . . . . . . 7
14 opeq1 3220 . . . . . . . . . . . 12
15 eceq1 5740 . . . . . . . . . . . 12
1614, 15syl 15 . . . . . . . . . . 11
1716oveq2d 5045 . . . . . . . . . 10
1817eleq1d 1983 . . . . . . . . 9
1918cbvabv 2457 . . . . . . . 8
20 1sr 7223 . . . . . . . . 9
2120elimel 3065 . . . . . . . 8
2219, 21supsrlem 7253 . . . . . . 7
2313, 22dedth 3054 . . . . . 6
2410, 23mpcom 32 . . . . 5
2524ex 419 . . . 4
2625exlimiv 1718 . . 3
271, 26sylbi 185 . 2
2827imp 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 2637  c0 2907  cif 3014  cop 3089   class class class wbr 3396  (class class class)co 5032  cec 5708  c1p 7000   cer 7006  cnr 7007  c1r 7009   cplr 7011   cltr 7013
This theorem is referenced by:  axpre-sup 7310
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 3481  ax-sep 3491  ax-nul 3500  ax-pow 3536  ax-pr 3560  ax-un 3836  ax-inf2 6289
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 2329  df-sbc 2496  df-csb 2578  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-pss 2650  df-nul 2908  df-if 3015  df-pw 3075  df-sn 3092  df-pr 3093  df-tp 3094  df-op 3095  df-uni 3247  df-int 3281  df-iun 3320  df-br 3397  df-opab 3450  df-tr 3465  df-eprel 3646  df-id 3650  df-po 3655  df-so 3669  df-fr 3689  df-we 3705  df-ord 3721  df-on 3722  df-lim 3723  df-suc 3724  df-om 4001  df-xp 4048  df-rel 4049  df-cnv 4050  df-co 4051  df-dm 4052  df-rn 4053  df-res 4054  df-ima 4055  df-fun 4056  df-fn 4057  df-f 4058  df-fv 4062  df-ov 5034  df-oprab 5035  df-mpt 5196  df-mpt2 5197  df-1st 5333  df-2nd 5334  df-rdg 5535  df-1o 5572  df-oadd 5576  df-omul 5577  df-er 5710  df-ec 5712  df-qs 5716  df-ni 7014  df-pli 7015  df-mi 7016  df-lti 7017  df-plpq 7050  df-mpq 7051  df-ltpq 7052  df-enq 7053  df-nq 7054  df-erq 7055  df-plq 7056  df-mq 7057  df-1nq 7058  df-rq 7059  df-ltnq 7060  df-np 7124  df-1p 7125  df-plp 7126  df-mp 7127  df-ltp 7128  df-plpr 7198  df-mpr 7199  df-enr 7200  df-nr 7201  df-plr 7202  df-mr 7203  df-ltr 7204  df-0r 7205  df-1r 7206  df-m1r 7207
Copyright terms: Public domain