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

Theorem supsr 8058
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 3094 . . 3
2 ltrelsr 8017 . . . . . . . . . . . . 13
32brel 4313 . . . . . . . . . . . 12
43simpld 438 . . . . . . . . . . 11
54ralimi 2365 . . . . . . . . . 10
6 dfss3 2825 . . . . . . . . . 10
75, 6sylibr 201 . . . . . . . . 9
87sseld 2834 . . . . . . . 8
98rexlimivw 2410 . . . . . . 7
109impcom 415 . . . . . 6
11 eleq1 2149 . . . . . . . . 9
1211anbi1d 679 . . . . . . . 8
1312imbi1d 306 . . . . . . 7
14 opeq1 3408 . . . . . . . . . . . 12
15 eceq1 6106 . . . . . . . . . . . 12
1614, 15syl 15 . . . . . . . . . . 11
1716oveq2d 5309 . . . . . . . . . 10
1817eleq1d 2155 . . . . . . . . 9
1918cbvabv 2630 . . . . . . . 8
20 1sr 8027 . . . . . . . . 9
2120elimel 3246 . . . . . . . 8
2219, 21supsrlem 8057 . . . . . . 7
2313, 22dedth 3235 . . . . . 6
2410, 23mpcom 32 . . . . 5
2524ex 419 . . . 4
2625exlimiv 1883 . . 3
271, 26sylbi 185 . 2
2827imp 414 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 357  wex 1450   wceq 1531   wcel 1533  cab 2077   wne 2207  wral 2299  wrex 2300   wss 2810  c0 3085  cif 3194  cop 3271   class class class wbr 3591  (class class class)co 5296  cec 6074  c1p 7806   cer 7812  cnr 7813  c1r 7815   cplr 7817   cltr 7819
This theorem is referenced by:  axpre-sup  8115
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-13 1538  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-sep 3687  ax-nul 3696  ax-pow 3732  ax-pr 3756  ax-un 4049  ax-inf2 6755
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1264  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-ral 2303  df-rex 2304  df-reu 2305  df-rab 2306  df-v 2502  df-sbc 2669  df-csb 2751  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3086  df-if 3195  df-pw 3256  df-sn 3274  df-pr 3275  df-tp 3276  df-op 3277  df-uni 3435  df-int 3469  df-iun 3511  df-br 3592  df-opab 3645  df-tr 3660  df-eprel 3844  df-id 3848  df-po 3853  df-so 3854  df-fr 3891  df-we 3893  df-ord 3934  df-on 3935  df-lim 3936  df-suc 3937  df-om 4216  df-xp 4263  df-rel 4264  df-cnv 4265  df-co 4266  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fun 4271  df-fn 4272  df-f 4273  df-f1 4274  df-fo 4275  df-f1o 4276  df-fv 4277  df-ov 5298  df-oprab 5299  df-mpt 5461  df-mpt2 5462  df-1st 5613  df-2nd 5614  df-recs 5814  df-rdg 5849  df-1o 5903  df-oadd 5907  df-omul 5908  df-er 6076  df-ec 6078  df-qs 6082  df-ni 7820  df-pli 7821  df-mi 7822  df-lti 7823  df-plpq 7856  df-mpq 7857  df-ltpq 7858  df-enq 7859  df-nq 7860  df-erq 7861  df-plq 7862  df-mq 7863  df-1nq 7864  df-rq 7865  df-ltnq 7866  df-np 7929  df-1p 7930  df-plp 7931  df-mp 7932  df-ltp 7933  df-plpr 8003  df-mpr 8004  df-enr 8005  df-nr 8006  df-plr 8007  df-mr 8008  df-ltr 8009  df-0r 8010  df-1r 8011  df-m1r 8012
Copyright terms: Public domain