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

Theorem axsup 9672
 Description: A nonempty, 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 9582 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 9582 . . . 4
213expia 1198 . . 3
3 ssel2 3504 . . . . . . . 8
4 ltxrlt 9667 . . . . . . . 8
53, 4sylan 471 . . . . . . 7
65an32s 802 . . . . . 6
76ralbidva 2903 . . . . 5
87rexbidva 2975 . . . 4
10 ltxrlt 9667 . . . . . . . . . . 11
1110ancoms 453 . . . . . . . . . 10
123, 11sylan 471 . . . . . . . . 9
1312an32s 802 . . . . . . . 8
1413notbid 294 . . . . . . 7
1514ralbidva 2903 . . . . . 6
164ancoms 453 . . . . . . . . 9
1716adantll 713 . . . . . . . 8
18 ssel2 3504 . . . . . . . . . . . 12
19 ltxrlt 9667 . . . . . . . . . . . . 13
2019ancoms 453 . . . . . . . . . . . 12
2118, 20sylan 471 . . . . . . . . . . 11
2221an32s 802 . . . . . . . . . 10
2322rexbidva 2975 . . . . . . . . 9
2423adantlr 714 . . . . . . . 8
2517, 24imbi12d 320 . . . . . . 7
2625ralbidva 2903 . . . . . 6
2715, 26anbi12d 710 . . . . 5
2827rexbidva 2975 . . . 4