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

Theorem axsup 8866
 Description: A non-empty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-sup 8783 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
Assertion
Ref Expression
axsup
Distinct variable group:   ,,,

Proof of Theorem axsup
StepHypRef Expression
1 ax-pre-sup 8783 . . . 4
213expia 1158 . . 3
3 ssel2 3150 . . . . . . . 8
4 ltxrlt 8861 . . . . . . . 8
53, 4sylan 459 . . . . . . 7
65an32s 782 . . . . . 6
76ralbidva 2534 . . . . 5
87rexbidva 2535 . . . 4
10 ltxrlt 8861 . . . . . . . . . . 11
1110ancoms 441 . . . . . . . . . 10
123, 11sylan 459 . . . . . . . . 9
1312an32s 782 . . . . . . . 8
1413notbid 287 . . . . . . 7
1514ralbidva 2534 . . . . . 6
164ancoms 441 . . . . . . . . 9
1716adantll 697 . . . . . . . 8
18 ssel2 3150 . . . . . . . . . . . 12
19 ltxrlt 8861 . . . . . . . . . . . . 13
2019ancoms 441 . . . . . . . . . . . 12
2118, 20sylan 459 . . . . . . . . . . 11
2221an32s 782 . . . . . . . . . 10
2322rexbidva 2535 . . . . . . . . 9
2423adantlr 698 . . . . . . . 8
2517, 24imbi12d 313 . . . . . . 7
2625ralbidva 2534 . . . . . 6
2715, 26anbi12d 694 . . . . 5
2827rexbidva 2535 . . . 4