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 A x y A y x x y A ¬ x < y y y < x z A y < z

Proof

Step Hyp Ref Expression
1 ssel A y A y
2 leloe y x y x y < x y = x
3 2 expcom x y y x y < x y = x
4 1 3 syl9 A x y A y x y < x y = x
5 4 imp31 A x y A y x y < x y = x
6 5 ralbidva A x y A y x y A y < x y = x
7 6 rexbidva A x y A y x x y A y < x y = x
8 7 anbi2d A A x y A y x A x y A y < x y = x
9 8 pm5.32i A A x y A y x A A x y A y < x y = x
10 3anass A A x y A y x A A x y A y x
11 3anass A A x y A y < x y = x A A x y A y < x y = x
12 9 10 11 3bitr4i A A x y A y x A A x y A y < x y = x
13 sup2 A A x y A y < x y = x x y A ¬ x < y y y < x z A y < z
14 12 13 sylbi A A x y A y x x y A ¬ x < y y y < x z A y < z