Axiom ax-pre-sup 10014

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 9990. Note: Normally new proofs would use axsup 10113. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)

Assertion

Ref	Expression
ax-pre-sup	|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <RR x ) -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )

Distinct variable group:   x, y, z, A

Detailed syntax breakdown of Axiom ax-pre-sup

Step	Hyp	Ref	Expression
1		cA	. . . 4 class A
2		cr 9935	. . . 4 class RR
3	1, 2	wss 3574	. . 3 wff A C_ RR
4		c0 3915	. . . 4 class (/)
5	1, 4	wne 2794	. . 3 wff A =/= (/)
6		vy	. . . . . . 7 setvar y
7	6	cv 1482	. . . . . 6 class y
8		vx	. . . . . . 7 setvar x
9	8	cv 1482	. . . . . 6 class x
10		cltrr 9940	. . . . . 6 class <RR
11	7, 9, 10	wbr 4653	. . . . 5 wff y <RR x
12	11, 6, 1	wral 2912	. . . 4 wff A. y e. A y <RR x
13	12, 8, 2	wrex 2913	. . 3 wff E. x e. RR A. y e. A y <RR x
14	3, 5, 13	w3a 1037	. 2 wff ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <RR x )
15	9, 7, 10	wbr 4653	. . . . . 6 wff x <RR y
16	15	wn 3	. . . . 5 wff -. x <RR y
17	16, 6, 1	wral 2912	. . . 4 wff A. y e. A -. x <RR y
18		vz	. . . . . . . . 9 setvar z
19	18	cv 1482	. . . . . . . 8 class z
20	7, 19, 10	wbr 4653	. . . . . . 7 wff y <RR z
21	20, 18, 1	wrex 2913	. . . . . 6 wff E. z e. A y <RR z
22	11, 21	wi 4	. . . . 5 wff ( y <RR x -> E. z e. A y <RR z )
23	22, 6, 2	wral 2912	. . . 4 wff A. y e. RR ( y <RR x -> E. z e. A y <RR z )
24	17, 23	wa 384	. . 3 wff ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) )
25	24, 8, 2	wrex 2913	. 2 wff E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) )
26	14, 25	wi 4	1 wff ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <RR x ) -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )

This axiom is referenced by:  axsup  10113