Metamath Proof Explorer


Theorem sup2

Description: A nonempty, bounded-above set of reals has a supremum. Stronger version of completeness axiom (it has a slightly weaker antecedent). (Contributed by NM, 19-Jan-1997)

Ref Expression
Assertion sup2 A A x y A y < x y = x x y A ¬ x < y y y < x z A y < z

Proof

Step Hyp Ref Expression
1 peano2re x x + 1
2 1 adantr x y A y < x y = x x + 1
3 2 a1i A x y A y < x y = x x + 1
4 ssel A y A y
5 ltp1 x x < x + 1
6 1 ancli x x x + 1
7 lttr y x x + 1 y < x x < x + 1 y < x + 1
8 7 3expb y x x + 1 y < x x < x + 1 y < x + 1
9 6 8 sylan2 y x y < x x < x + 1 y < x + 1
10 5 9 sylan2i y x y < x x y < x + 1
11 10 exp4b y x y < x x y < x + 1
12 11 com34 y x x y < x y < x + 1
13 12 pm2.43d y x y < x y < x + 1
14 13 imp y x y < x y < x + 1
15 breq1 y = x y < x + 1 x < x + 1
16 5 15 syl5ibrcom x y = x y < x + 1
17 16 adantl y x y = x y < x + 1
18 14 17 jaod y x y < x y = x y < x + 1
19 18 ex y x y < x y = x y < x + 1
20 4 19 syl6 A y A x y < x y = x y < x + 1
21 20 com23 A x y A y < x y = x y < x + 1
22 21 imp A x y A y < x y = x y < x + 1
23 22 a2d A x y A y < x y = x y A y < x + 1
24 23 ralimdv2 A x y A y < x y = x y A y < x + 1
25 24 expimpd A x y A y < x y = x y A y < x + 1
26 3 25 jcad A x y A y < x y = x x + 1 y A y < x + 1
27 ovex x + 1 V
28 eleq1 z = x + 1 z x + 1
29 breq2 z = x + 1 y < z y < x + 1
30 29 ralbidv z = x + 1 y A y < z y A y < x + 1
31 28 30 anbi12d z = x + 1 z y A y < z x + 1 y A y < x + 1
32 27 31 spcev x + 1 y A y < x + 1 z z y A y < z
33 26 32 syl6 A x y A y < x y = x z z y A y < z
34 33 exlimdv A x x y A y < x y = x z z y A y < z
35 eleq1 z = x z x
36 breq2 z = x y < z y < x
37 36 ralbidv z = x y A y < z y A y < x
38 35 37 anbi12d z = x z y A y < z x y A y < x
39 38 cbvexvw z z y A y < z x x y A y < x
40 34 39 syl6ib A x x y A y < x y = x x x y A y < x
41 df-rex x y A y < x y = x x x y A y < x y = x
42 df-rex x y A y < x x x y A y < x
43 40 41 42 3imtr4g A x y A y < x y = x x y A y < x
44 43 adantr A A x y A y < x y = x x y A y < x
45 44 imdistani A A x y A y < x y = x A A x y A y < x
46 df-3an A A x y A y < x y = x A A x y A y < x y = x
47 df-3an A A x y A y < x A A x y A y < x
48 45 46 47 3imtr4i A A x y A y < x y = x A A x y A y < x
49 axsup A A x y A y < x x y A ¬ x < y y y < x z A y < z
50 48 49 syl A A x y A y < x y = x x y A ¬ x < y y y < x z A y < z