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 C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y  E. x e. RR ( A. y e. A -. x  E. z e. A y

Proof

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