Theorem axsup

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 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005)

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

Proof

Step	Hyp	Ref	Expression
1		ax-pre-sup	|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y E. x e. RR ( A. y e. A -. x E. z e. A y
2	1	3expia	|- ( ( A C_ RR /\ A =/= (/) ) -> ( E. x e. RR A. y e. A y E. x e. RR ( A. y e. A -. x E. z e. A y
3		ssel2	|- ( ( A C_ RR /\ y e. A ) -> y e. RR )
4		ltxrlt	|- ( ( y e. RR /\ x e. RR ) -> ( y < x <-> y
5	3 4	sylan	|- ( ( ( A C_ RR /\ y e. A ) /\ x e. RR ) -> ( y < x <-> y
6	5	an32s	|- ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( y < x <-> y
7	6	ralbidva	|- ( ( A C_ RR /\ x e. RR ) -> ( A. y e. A y < x <-> A. y e. A y
8	7	rexbidva	|- ( A C_ RR -> ( E. x e. RR A. y e. A y < x <-> E. x e. RR A. y e. A y
9	8	adantr	|- ( ( A C_ RR /\ A =/= (/) ) -> ( E. x e. RR A. y e. A y < x <-> E. x e. RR A. y e. A y
10		ltxrlt	|- ( ( x e. RR /\ y e. RR ) -> ( x < y <-> x
11	10	ancoms	|- ( ( y e. RR /\ x e. RR ) -> ( x < y <-> x
12	3 11	sylan	|- ( ( ( A C_ RR /\ y e. A ) /\ x e. RR ) -> ( x < y <-> x
13	12	an32s	|- ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( x < y <-> x
14	13	notbid	|- ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( -. x < y <-> -. x
15	14	ralbidva	|- ( ( A C_ RR /\ x e. RR ) -> ( A. y e. A -. x < y <-> A. y e. A -. x
16	4	ancoms	|- ( ( x e. RR /\ y e. RR ) -> ( y < x <-> y
17	16	adantll	|- ( ( ( A C_ RR /\ x e. RR ) /\ y e. RR ) -> ( y < x <-> y
18		ssel2	|- ( ( A C_ RR /\ z e. A ) -> z e. RR )
19		ltxrlt	|- ( ( y e. RR /\ z e. RR ) -> ( y < z <-> y
20	19	ancoms	|- ( ( z e. RR /\ y e. RR ) -> ( y < z <-> y
21	18 20	sylan	|- ( ( ( A C_ RR /\ z e. A ) /\ y e. RR ) -> ( y < z <-> y
22	21	an32s	|- ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( y < z <-> y
23	22	rexbidva	|- ( ( A C_ RR /\ y e. RR ) -> ( E. z e. A y < z <-> E. z e. A y
24	23	adantlr	|- ( ( ( A C_ RR /\ x e. RR ) /\ y e. RR ) -> ( E. z e. A y < z <-> E. z e. A y
25	17 24	imbi12d	|- ( ( ( A C_ RR /\ x e. RR ) /\ y e. RR ) -> ( ( y < x -> E. z e. A y < z ) <-> ( y E. z e. A y
26	25	ralbidva	|- ( ( A C_ RR /\ x e. RR ) -> ( A. y e. RR ( y < x -> E. z e. A y < z ) <-> A. y e. RR ( y E. z e. A y
27	15 26	anbi12d	|- ( ( A C_ RR /\ x e. RR ) -> ( ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) <-> ( A. y e. A -. x E. z e. A y
28	27	rexbidva	|- ( A C_ RR -> ( E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) <-> E. x e. RR ( A. y e. A -. x E. z e. A y
29	28	adantr	|- ( ( A C_ RR /\ A =/= (/) ) -> ( E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) <-> E. x e. RR ( A. y e. A -. x E. z e. A y
30	2 9 29	3imtr4d	|- ( ( A C_ RR /\ A =/= (/) ) -> ( E. x e. RR A. y e. A y < x -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) ) )
31	30	3impia	|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y < x ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )