Metamath Proof Explorer


Theorem axpre-sup

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. Note: The more general version with ordering on extended reals is axsup . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup . (Contributed by NM, 19-May-1996) (Revised by Mario Carneiro, 16-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion axpre-sup 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 elreal2 x 1 st x 𝑹 x = 1 st x 0 𝑹
2 1 simplbi x 1 st x 𝑹
3 2 adantl A A x 1 st x 𝑹
4 fo1st 1 st : V onto V
5 fof 1 st : V onto V 1 st : V V
6 ffn 1 st : V V 1 st Fn V
7 4 5 6 mp2b 1 st Fn V
8 ssv A V
9 fvelimab 1 st Fn V A V w 1 st A y A 1 st y = w
10 7 8 9 mp2an w 1 st A y A 1 st y = w
11 r19.29 y A y < x y A 1 st y = w y A y < x 1 st y = w
12 ssel2 A y A y
13 ltresr2 y x y < x 1 st y < 𝑹 1 st x
14 breq1 1 st y = w 1 st y < 𝑹 1 st x w < 𝑹 1 st x
15 13 14 sylan9bb y x 1 st y = w y < x w < 𝑹 1 st x
16 15 biimpd y x 1 st y = w y < x w < 𝑹 1 st x
17 16 exp31 y x 1 st y = w y < x w < 𝑹 1 st x
18 12 17 syl A y A x 1 st y = w y < x w < 𝑹 1 st x
19 18 imp4b A y A x 1 st y = w y < x w < 𝑹 1 st x
20 19 ancomsd A y A x y < x 1 st y = w w < 𝑹 1 st x
21 20 an32s A x y A y < x 1 st y = w w < 𝑹 1 st x
22 21 rexlimdva A x y A y < x 1 st y = w w < 𝑹 1 st x
23 11 22 syl5 A x y A y < x y A 1 st y = w w < 𝑹 1 st x
24 23 expd A x y A y < x y A 1 st y = w w < 𝑹 1 st x
25 10 24 syl7bi A x y A y < x w 1 st A w < 𝑹 1 st x
26 25 impr A x y A y < x w 1 st A w < 𝑹 1 st x
27 26 adantlr A A x y A y < x w 1 st A w < 𝑹 1 st x
28 27 ralrimiv A A x y A y < x w 1 st A w < 𝑹 1 st x
29 28 expr A A x y A y < x w 1 st A w < 𝑹 1 st x
30 brralrspcev 1 st x 𝑹 w 1 st A w < 𝑹 1 st x v 𝑹 w 1 st A w < 𝑹 v
31 3 29 30 syl6an A A x y A y < x v 𝑹 w 1 st A w < 𝑹 v
32 31 rexlimdva A A x y A y < x v 𝑹 w 1 st A w < 𝑹 v
33 n0 A y y A
34 fnfvima 1 st Fn V A V y A 1 st y 1 st A
35 7 8 34 mp3an12 y A 1 st y 1 st A
36 35 ne0d y A 1 st A
37 36 exlimiv y y A 1 st A
38 33 37 sylbi A 1 st A
39 supsr 1 st A v 𝑹 w 1 st A w < 𝑹 v v 𝑹 w 1 st A ¬ v < 𝑹 w w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u
40 39 ex 1 st A v 𝑹 w 1 st A w < 𝑹 v v 𝑹 w 1 st A ¬ v < 𝑹 w w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u
41 38 40 syl A v 𝑹 w 1 st A w < 𝑹 v v 𝑹 w 1 st A ¬ v < 𝑹 w w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u
42 41 adantl A A v 𝑹 w 1 st A w < 𝑹 v v 𝑹 w 1 st A ¬ v < 𝑹 w w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u
43 breq2 w = 1 st y v < 𝑹 w v < 𝑹 1 st y
44 43 notbid w = 1 st y ¬ v < 𝑹 w ¬ v < 𝑹 1 st y
45 44 rspccv w 1 st A ¬ v < 𝑹 w 1 st y 1 st A ¬ v < 𝑹 1 st y
46 35 45 syl5com y A w 1 st A ¬ v < 𝑹 w ¬ v < 𝑹 1 st y
47 46 adantl A y A w 1 st A ¬ v < 𝑹 w ¬ v < 𝑹 1 st y
48 elreal2 y 1 st y 𝑹 y = 1 st y 0 𝑹
49 48 simprbi y y = 1 st y 0 𝑹
50 49 breq2d y v 0 𝑹 < y v 0 𝑹 < 1 st y 0 𝑹
51 ltresr v 0 𝑹 < 1 st y 0 𝑹 v < 𝑹 1 st y
52 50 51 bitrdi y v 0 𝑹 < y v < 𝑹 1 st y
53 12 52 syl A y A v 0 𝑹 < y v < 𝑹 1 st y
54 53 notbid A y A ¬ v 0 𝑹 < y ¬ v < 𝑹 1 st y
55 47 54 sylibrd A y A w 1 st A ¬ v < 𝑹 w ¬ v 0 𝑹 < y
56 55 ralrimdva A w 1 st A ¬ v < 𝑹 w y A ¬ v 0 𝑹 < y
57 56 ad2antrr A A v 𝑹 w 1 st A ¬ v < 𝑹 w y A ¬ v 0 𝑹 < y
58 49 breq1d y y < v 0 𝑹 1 st y 0 𝑹 < v 0 𝑹
59 ltresr 1 st y 0 𝑹 < v 0 𝑹 1 st y < 𝑹 v
60 58 59 bitrdi y y < v 0 𝑹 1 st y < 𝑹 v
61 48 simplbi y 1 st y 𝑹
62 breq1 w = 1 st y w < 𝑹 v 1 st y < 𝑹 v
63 breq1 w = 1 st y w < 𝑹 u 1 st y < 𝑹 u
64 63 rexbidv w = 1 st y u 1 st A w < 𝑹 u u 1 st A 1 st y < 𝑹 u
65 62 64 imbi12d w = 1 st y w < 𝑹 v u 1 st A w < 𝑹 u 1 st y < 𝑹 v u 1 st A 1 st y < 𝑹 u
66 65 rspccv w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u 1 st y 𝑹 1 st y < 𝑹 v u 1 st A 1 st y < 𝑹 u
67 61 66 syl5 w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u y 1 st y < 𝑹 v u 1 st A 1 st y < 𝑹 u
68 67 com3l y 1 st y < 𝑹 v w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u u 1 st A 1 st y < 𝑹 u
69 60 68 sylbid y y < v 0 𝑹 w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u u 1 st A 1 st y < 𝑹 u
70 69 adantr y A y < v 0 𝑹 w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u u 1 st A 1 st y < 𝑹 u
71 fvelimab 1 st Fn V A V u 1 st A z A 1 st z = u
72 7 8 71 mp2an u 1 st A z A 1 st z = u
73 ssel2 A z A z
74 ltresr2 y z y < z 1 st y < 𝑹 1 st z
75 73 74 sylan2 y A z A y < z 1 st y < 𝑹 1 st z
76 breq2 1 st z = u 1 st y < 𝑹 1 st z 1 st y < 𝑹 u
77 75 76 sylan9bb y A z A 1 st z = u y < z 1 st y < 𝑹 u
78 77 exbiri y A z A 1 st z = u 1 st y < 𝑹 u y < z
79 78 expr y A z A 1 st z = u 1 st y < 𝑹 u y < z
80 79 com4r 1 st y < 𝑹 u y A z A 1 st z = u y < z
81 80 imp 1 st y < 𝑹 u y A z A 1 st z = u y < z
82 81 reximdvai 1 st y < 𝑹 u y A z A 1 st z = u z A y < z
83 72 82 syl5bi 1 st y < 𝑹 u y A u 1 st A z A y < z
84 83 expcom y A 1 st y < 𝑹 u u 1 st A z A y < z
85 84 com23 y A u 1 st A 1 st y < 𝑹 u z A y < z
86 85 rexlimdv y A u 1 st A 1 st y < 𝑹 u z A y < z
87 70 86 syl6d y A y < v 0 𝑹 w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u z A y < z
88 87 com23 y A w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u y < v 0 𝑹 z A y < z
89 88 ex y A w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u y < v 0 𝑹 z A y < z
90 89 com3l A w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u y y < v 0 𝑹 z A y < z
91 90 ad2antrr A A v 𝑹 w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u y y < v 0 𝑹 z A y < z
92 91 ralrimdv A A v 𝑹 w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u y y < v 0 𝑹 z A y < z
93 opelreal v 0 𝑹 v 𝑹
94 93 biimpri v 𝑹 v 0 𝑹
95 94 adantl A A v 𝑹 v 0 𝑹
96 breq1 x = v 0 𝑹 x < y v 0 𝑹 < y
97 96 notbid x = v 0 𝑹 ¬ x < y ¬ v 0 𝑹 < y
98 97 ralbidv x = v 0 𝑹 y A ¬ x < y y A ¬ v 0 𝑹 < y
99 breq2 x = v 0 𝑹 y < x y < v 0 𝑹
100 99 imbi1d x = v 0 𝑹 y < x z A y < z y < v 0 𝑹 z A y < z
101 100 ralbidv x = v 0 𝑹 y y < x z A y < z y y < v 0 𝑹 z A y < z
102 98 101 anbi12d x = v 0 𝑹 y A ¬ x < y y y < x z A y < z y A ¬ v 0 𝑹 < y y y < v 0 𝑹 z A y < z
103 102 rspcev v 0 𝑹 y A ¬ v 0 𝑹 < y y y < v 0 𝑹 z A y < z x y A ¬ x < y y y < x z A y < z
104 103 ex v 0 𝑹 y A ¬ v 0 𝑹 < y y y < v 0 𝑹 z A y < z x y A ¬ x < y y y < x z A y < z
105 95 104 syl A A v 𝑹 y A ¬ v 0 𝑹 < y y y < v 0 𝑹 z A y < z x y A ¬ x < y y y < x z A y < z
106 57 92 105 syl2and A A v 𝑹 w 1 st A ¬ v < 𝑹 w w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u x y A ¬ x < y y y < x z A y < z
107 106 rexlimdva A A v 𝑹 w 1 st A ¬ v < 𝑹 w w 𝑹 w < 𝑹 v u 1 st A w < 𝑹 u x y A ¬ x < y y y < x z A y < z
108 32 42 107 3syld A A x y A y < x x y A ¬ x < y y y < x z A y < z
109 108 3impia A A x y A y < x x y A ¬ x < y y y < x z A y < z