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

Theorem supxrbnd 11614
 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 9684 . . . . 5
2 sstr 3440 . . . . 5
31, 2mpan2 677 . . . 4
4 supxrcl 11600 . . . . . . 7
5 pnfxr 11412 . . . . . . . . . 10
6 xrltne 11460 . . . . . . . . . 10
75, 6mp3an2 1352 . . . . . . . . 9
87necomd 2679 . . . . . . . 8
98ex 436 . . . . . . 7
104, 9syl 17 . . . . . 6
11 supxrunb2 11606 . . . . . . . . 9
12 ssel2 3427 . . . . . . . . . . . . . 14
1312adantlr 721 . . . . . . . . . . . . 13
14 rexr 9686 . . . . . . . . . . . . . 14
1514ad2antlr 733 . . . . . . . . . . . . 13
16 xrlenlt 9699 . . . . . . . . . . . . . 14
1716con2bid 331 . . . . . . . . . . . . 13
1813, 15, 17syl2anc 667 . . . . . . . . . . . 12
1918rexbidva 2898 . . . . . . . . . . 11
20 rexnal 2836 . . . . . . . . . . 11
2119, 20syl6bb 265 . . . . . . . . . 10
2221ralbidva 2824 . . . . . . . . 9
2311, 22bitr3d 259 . . . . . . . 8
24 ralnex 2834 . . . . . . . 8
2523, 24syl6bb 265 . . . . . . 7
2625necon2abid 2666 . . . . . 6
2710, 26sylibrd 238 . . . . 5
2827imp 431 . . . 4
293, 28sylan 474 . . 3