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

Theorem supsr 7003
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 2908 . . 3
2 vex 2338 . . . . . . . . . . . . 13
3 ltrelsr 6962 . . . . . . . . . . . . 13
42, 3brel 4059 . . . . . . . . . . . 12
54simpld 442 . . . . . . . . . . 11
65ralimi 2204 . . . . . . . . . 10
7 dfss3 2649 . . . . . . . . . 10
86, 7sylibr 201 . . . . . . . . 9
98sseld 2658 . . . . . . . 8
109rexlimivw 2249 . . . . . . 7
1110impcom 419 . . . . . 6
12 eleq1 1988 . . . . . . . . 9
1312anbi1d 686 . . . . . . . 8
1413imbi1d 308 . . . . . . 7
15 opeq1 3192 . . . . . . . . . . . 12
16 eceq1 5563 . . . . . . . . . . . 12
1715, 16syl 14 . . . . . . . . . . 11
1817oveq2d 4937 . . . . . . . . . 10
1918eleq1d 1994 . . . . . . . . 9
2019cbvabv 2465 . . . . . . . 8
21 1sr 6972 . . . . . . . . 9
2221elimel 3053 . . . . . . . 8
2320, 22supsrlem 7002 . . . . . . 7
2414, 23dedth 3042 . . . . . 6
2511, 24mpcom 31 . . . . 5
2625ex 423 . . . 4
2726exlimiv 1729 . . 3
281, 27sylbi 185 . 2
2928imp 418 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 360  wex 1346   wceq 1425   wcel 1427  cab 1916   wne 2047  wral 2138  wrex 2139   wss 2634  c0 2899  cif 3004  cop 3077   class class class wbr 3358  (class class class)co 4924  cec 5535  c1p 6749   cer 6755  cnr 6756  c1r 6758   cplr 6760   cltr 6762
This theorem is referenced by:  axpre-sup 7059
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-13 1433  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3795  ax-inf2 6078
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3or 913  df-3an 914  df-tru 1320  df-ex 1347  df-sb 1602  df-eu 1829  df-mo 1830  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-ral 2142  df-rex 2143  df-reu 2144  df-rab 2145  df-v 2337  df-sbc 2502  df-csb 2577  df-dif 2637  df-un 2639  df-in 2641  df-ss 2643  df-pss 2645  df-nul 2900  df-if 3005  df-pw 3063  df-sn 3080  df-pr 3081  df-tp 3082  df-op 3083  df-uni 3214  df-int 3248  df-iun 3286  df-br 3359  df-opab 3413  df-tr 3428  df-eprel 3608  df-id 3611  df-po 3616  df-so 3630  df-fr 3649  df-we 3665  df-ord 3681  df-on 3682  df-lim 3683  df-suc 3684  df-om 3958  df-xp 4005  df-rel 4006  df-cnv 4007  df-co 4008  df-dm 4009  df-rn 4010  df-res 4011  df-ima 4012  df-fun 4013  df-fn 4014  df-f 4015  df-fv 4019  df-ov 4926  df-oprab 4927  df-mpt 5063  df-mpt2 5064  df-1st 5173  df-2nd 5174  df-rdg 5363  df-1o 5400  df-oadd 5404  df-omul 5405  df-er 5537  df-ec 5539  df-qs 5543  df-ni 6763  df-pli 6764  df-mi 6765  df-lti 6766  df-plpq 6799  df-mpq 6800  df-ltpq 6801  df-enq 6802  df-nq 6803  df-erq 6804  df-plq 6805  df-mq 6806  df-1nq 6807  df-rq 6808  df-ltnq 6809  df-np 6873  df-1p 6874  df-plp 6875  df-mp 6876  df-ltp 6877  df-plpr 6947  df-mpr 6948  df-enr 6949  df-nr 6950  df-plr 6951  df-mr 6952  df-ltr 6953  df-0r 6954  df-1r 6955  df-m1r 6956
Copyright terms: Public domain