Metamath Proof Explorer

Theorem sup3

Description: A version of the completeness axiom for reals. (Contributed by NM, 12-Oct-2004)

		Ref	Expression
	Assertion	sup3	\|- ( ( 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		ssel	\|- ( A C_ RR -> ( y e. A -> y e. RR ) )
2		leloe	\|- ( ( y e. RR /\ x e. RR ) -> ( y <_ x <-> ( y < x \/ y = x ) ) )
3	2	expcom	\|- ( x e. RR -> ( y e. RR -> ( y <_ x <-> ( y < x \/ y = x ) ) ) )
4	1 3	syl9	\|- ( A C_ RR -> ( x e. RR -> ( y e. A -> ( y <_ x <-> ( y < x \/ y = x ) ) ) ) )
5	4	imp31	\|- ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( y <_ x <-> ( y < x \/ y = x ) ) )
6	5	ralbidva	\|- ( ( A C_ RR /\ x e. RR ) -> ( A. y e. A y <_ x <-> A. y e. A ( y < x \/ y = x ) ) )
7	6	rexbidva	\|- ( A C_ RR -> ( E. x e. RR A. y e. A y <_ x <-> E. x e. RR A. y e. A ( y < x \/ y = x ) ) )
8	7	anbi2d	\|- ( A C_ RR -> ( ( A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) <-> ( A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) ) )
9	8	pm5.32i	\|- ( ( A C_ RR /\ ( A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) ) <-> ( A C_ RR /\ ( A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) ) )
10		3anass	\|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) <-> ( A C_ RR /\ ( A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) ) )
11		3anass	\|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) <-> ( A C_ RR /\ ( A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) ) )
12	9 10 11	3bitr4i	\|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) <-> ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) )
13		sup2	\|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A ( y < x \/ y = x ) ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
14	12 13	sylbi	\|- ( ( 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 ) ) )