Metamath Proof Explorer


Theorem supxrunb1

Description: The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion supxrunb1 A * x y A x y sup A * < = +∞

Proof

Step Hyp Ref Expression
1 ssel A * z A z *
2 pnfnlt z * ¬ +∞ < z
3 1 2 syl6 A * z A ¬ +∞ < z
4 3 ralrimiv A * z A ¬ +∞ < z
5 4 adantr A * x y A x y z A ¬ +∞ < z
6 peano2re z z + 1
7 breq1 x = z + 1 x y z + 1 y
8 7 rexbidv x = z + 1 y A x y y A z + 1 y
9 8 rspcva z + 1 x y A x y y A z + 1 y
10 9 adantrr z + 1 x y A x y A * y A z + 1 y
11 10 ancoms x y A x y A * z + 1 y A z + 1 y
12 6 11 sylan2 x y A x y A * z y A z + 1 y
13 ssel2 A * y A y *
14 ltp1 z z < z + 1
15 14 adantr z y * z < z + 1
16 6 ancli z z z + 1
17 rexr z z *
18 rexr z + 1 z + 1 *
19 xrltletr z * z + 1 * y * z < z + 1 z + 1 y z < y
20 18 19 syl3an2 z * z + 1 y * z < z + 1 z + 1 y z < y
21 17 20 syl3an1 z z + 1 y * z < z + 1 z + 1 y z < y
22 21 3expa z z + 1 y * z < z + 1 z + 1 y z < y
23 16 22 sylan z y * z < z + 1 z + 1 y z < y
24 15 23 mpand z y * z + 1 y z < y
25 24 ancoms y * z z + 1 y z < y
26 13 25 sylan A * y A z z + 1 y z < y
27 26 an32s A * z y A z + 1 y z < y
28 27 reximdva A * z y A z + 1 y y A z < y
29 28 adantll x y A x y A * z y A z + 1 y y A z < y
30 12 29 mpd x y A x y A * z y A z < y
31 30 exp31 x y A x y A * z y A z < y
32 31 a1dd x y A x y A * z < +∞ z y A z < y
33 32 com4r z x y A x y A * z < +∞ y A z < y
34 33 com13 A * x y A x y z z < +∞ y A z < y
35 34 imp A * x y A x y z z < +∞ y A z < y
36 35 ralrimiv A * x y A x y z z < +∞ y A z < y
37 5 36 jca A * x y A x y z A ¬ +∞ < z z z < +∞ y A z < y
38 pnfxr +∞ *
39 supxr A * +∞ * z A ¬ +∞ < z z z < +∞ y A z < y sup A * < = +∞
40 38 39 mpanl2 A * z A ¬ +∞ < z z z < +∞ y A z < y sup A * < = +∞
41 37 40 syldan A * x y A x y sup A * < = +∞
42 41 ex A * x y A x y sup A * < = +∞
43 rexr x x *
44 43 ad2antlr A * x sup A * < = +∞ x *
45 ltpnf x x < +∞
46 breq2 sup A * < = +∞ x < sup A * < x < +∞
47 45 46 syl5ibr sup A * < = +∞ x x < sup A * <
48 47 impcom x sup A * < = +∞ x < sup A * <
49 48 adantll A * x sup A * < = +∞ x < sup A * <
50 xrltso < Or *
51 50 a1i A * x sup A * < = +∞ < Or *
52 xrsupss A * z * w A ¬ z < w w * w < z y A w < y
53 52 ad2antrr A * x sup A * < = +∞ z * w A ¬ z < w w * w < z y A w < y
54 51 53 suplub A * x sup A * < = +∞ x * x < sup A * < y A x < y
55 44 49 54 mp2and A * x sup A * < = +∞ y A x < y
56 55 ex A * x sup A * < = +∞ y A x < y
57 43 ad2antlr A * x y A x *
58 13 adantlr A * x y A y *
59 xrltle x * y * x < y x y
60 57 58 59 syl2anc A * x y A x < y x y
61 60 reximdva A * x y A x < y y A x y
62 56 61 syld A * x sup A * < = +∞ y A x y
63 62 ralrimdva A * sup A * < = +∞ x y A x y
64 42 63 impbid A * x y A x y sup A * < = +∞