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

Theorem supsr 7104
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 2907 . . 3
2 vex 2325 . . . . . . . . . . . . 13
3 ltrelsr 7063 . . . . . . . . . . . . 13
42, 3brel 4058 . . . . . . . . . . . 12
54simpld 437 . . . . . . . . . . 11
65ralimi 2191 . . . . . . . . . 10
7 dfss3 2647 . . . . . . . . . 10
86, 7sylibr 200 . . . . . . . . 9
98sseld 2656 . . . . . . . 8
109rexlimivw 2236 . . . . . . 7
1110impcom 414 . . . . . 6
12 eleq1 1976 . . . . . . . . 9
1312anbi1d 678 . . . . . . . 8
1413imbi1d 305 . . . . . . 7
15 opeq1 3192 . . . . . . . . . . . 12
16 eceq1 5628 . . . . . . . . . . . 12
1715, 16syl 14 . . . . . . . . . . 11
1817oveq2d 4957 . . . . . . . . . 10
1918eleq1d 1982 . . . . . . . . 9
2019cbvabv 2452 . . . . . . . 8
21 1sr 7073 . . . . . . . . 9
2221elimel 3052 . . . . . . . 8
2320, 22supsrlem 7103 . . . . . . 7
2414, 23dedth 3041 . . . . . 6
2511, 24mpcom 31 . . . . 5
2625ex 418 . . . 4
2726exlimiv 1717 . . 3
281, 27sylbi 184 . 2
2928imp 413 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 356  wex 1334   wceq 1413   wcel 1415  cab 1904   wne 2034  wral 2125  wrex 2126   wss 2632  c0 2898  cif 3003  cop 3076   class class class wbr 3358  (class class class)co 4944  cec 5596  c1p 6850   cer 6856  cnr 6857  c1r 6859   cplr 6861   cltr 6863
This theorem is referenced by:  axpre-sup 7160
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-13 1421  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3797  ax-inf2 6154
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3or 899  df-3an 900  df-tru 1308  df-ex 1335  df-sb 1590  df-eu 1817  df-mo 1818  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-ral 2129  df-rex 2130  df-reu 2131  df-rab 2132  df-v 2324  df-sbc 2491  df-csb 2573  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-pss 2643  df-nul 2899  df-if 3004  df-pw 3062  df-sn 3079  df-pr 3080  df-tp 3081  df-op 3082  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 3650  df-we 3666  df-ord 3682  df-on 3683  df-lim 3684  df-suc 3685  df-om 3962  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-fv 4023  df-ov 4946  df-oprab 4947  df-mpt 5106  df-mpt2 5107  df-1st 5231  df-2nd 5232  df-rdg 5424  df-1o 5461  df-oadd 5465  df-omul 5466  df-er 5598  df-ec 5600  df-qs 5604  df-ni 6864  df-pli 6865  df-mi 6866  df-lti 6867  df-plpq 6900  df-mpq 6901  df-ltpq 6902  df-enq 6903  df-nq 6904  df-erq 6905  df-plq 6906  df-mq 6907  df-1nq 6908  df-rq 6909  df-ltnq 6910  df-np 6974  df-1p 6975  df-plp 6976  df-mp 6977  df-ltp 6978  df-plpr 7048  df-mpr 7049  df-enr 7050  df-nr 7051  df-plr 7052  df-mr 7053  df-ltr 7054  df-0r 7055  df-1r 7056  df-m1r 7057
Copyright terms: Public domain