Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  supxrbnd Structured version   Unicode version

Theorem supxrbnd 10899
 Description: The supremum of a bounded-above nonempty set of reals is real. (Contributed by NM, 19-Jan-2006.)
Assertion
Ref Expression
supxrbnd

Proof of Theorem supxrbnd
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ressxr 9121 . . . . 5
2 sstr 3348 . . . . 5
31, 2mpan2 653 . . . 4
4 supxrcl 10885 . . . . . . 7
5 pnfxr 10705 . . . . . . . . . 10
6 xrltne 10745 . . . . . . . . . 10
75, 6mp3an2 1267 . . . . . . . . 9
87necomd 2681 . . . . . . . 8
98ex 424 . . . . . . 7
104, 9syl 16 . . . . . 6
11 supxrunb2 10891 . . . . . . . . 9
12 ssel2 3335 . . . . . . . . . . . . . 14
1312adantlr 696 . . . . . . . . . . . . 13
14 rexr 9122 . . . . . . . . . . . . . 14
1514ad2antlr 708 . . . . . . . . . . . . 13
16 xrlenlt 9135 . . . . . . . . . . . . . 14
1716con2bid 320 . . . . . . . . . . . . 13
1813, 15, 17syl2anc 643 . . . . . . . . . . . 12
1918rexbidva 2714 . . . . . . . . . . 11
20 rexnal 2708 . . . . . . . . . . 11
2119, 20syl6bb 253 . . . . . . . . . 10
2221ralbidva 2713 . . . . . . . . 9
2311, 22bitr3d 247 . . . . . . . 8
24 ralnex 2707 . . . . . . . 8
2523, 24syl6bb 253 . . . . . . 7
2625necon2abid 2655 . . . . . 6
2710, 26sylibrd 226 . . . . 5
2827imp 419 . . . 4
293, 28sylan 458 . . 3