Metamath Proof Explorer


Axiom ax-pre-sup

Description: A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by Theorem axpre-sup . Note: Normally new proofs would use axsup . (New usage is discouraged.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion ax-pre-sup A A x y A y < x x y A ¬ x < y y y < x z A y < z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cr class
2 0 1 wss wff A
3 c0 class
4 0 3 wne wff A
5 vx setvar x
6 vy setvar y
7 6 cv setvar y
8 cltrr class <
9 5 cv setvar x
10 7 9 8 wbr wff y < x
11 10 6 0 wral wff y A y < x
12 11 5 1 wrex wff x y A y < x
13 2 4 12 w3a wff A A x y A y < x
14 9 7 8 wbr wff x < y
15 14 wn wff ¬ x < y
16 15 6 0 wral wff y A ¬ x < y
17 vz setvar z
18 17 cv setvar z
19 7 18 8 wbr wff y < z
20 19 17 0 wrex wff z A y < z
21 10 20 wi wff y < x z A y < z
22 21 6 1 wral wff y y < x z A y < z
23 16 22 wa wff y A ¬ x < y y y < x z A y < z
24 23 5 1 wrex wff x y A ¬ x < y y y < x z A y < z
25 13 24 wi wff A A x y A y < x x y A ¬ x < y y y < x z A y < z