Metamath Proof Explorer

Theorem supxrunb3

Description: The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion supxrunb3 
|- ( A C_ RR* -> ( A. x e. RR E. y e. A x <_ y <-> sup ( A , RR* , < ) = +oo ) )

Proof

Step Hyp Ref Expression
1 peano2re 
 |-  ( w e. RR -> ( w + 1 ) e. RR )
2 1 adantl 
 |-  ( ( A. x e. RR E. y e. A x <_ y /\ w e. RR ) -> ( w + 1 ) e. RR )
3 simpl 
 |-  ( ( A. x e. RR E. y e. A x <_ y /\ w e. RR ) -> A. x e. RR E. y e. A x <_ y )
4 breq1 
 |-  ( x = ( w + 1 ) -> ( x <_ y <-> ( w + 1 ) <_ y ) )
5 4 rexbidv 
 |-  ( x = ( w + 1 ) -> ( E. y e. A x <_ y <-> E. y e. A ( w + 1 ) <_ y ) )
6 5 rspcva 
 |-  ( ( ( w + 1 ) e. RR /\ A. x e. RR E. y e. A x <_ y ) -> E. y e. A ( w + 1 ) <_ y )
7 2 3 6 syl2anc 
 |-  ( ( A. x e. RR E. y e. A x <_ y /\ w e. RR ) -> E. y e. A ( w + 1 ) <_ y )
8 7 adantll 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A x <_ y ) /\ w e. RR ) -> E. y e. A ( w + 1 ) <_ y )
9 nfv 
 |-  F/ y A C_ RR*
10 nfcv 
 |-  F/_ y RR
11 nfre1 
 |-  F/ y E. y e. A x <_ y
12 10 11 nfralw 
 |-  F/ y A. x e. RR E. y e. A x <_ y
13 9 12 nfan 
 |-  F/ y ( A C_ RR* /\ A. x e. RR E. y e. A x <_ y )
14 nfv 
 |-  F/ y w e. RR
15 13 14 nfan 
 |-  F/ y ( ( A C_ RR* /\ A. x e. RR E. y e. A x <_ y ) /\ w e. RR )
16 simp1r 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A /\ ( w + 1 ) <_ y ) -> w e. RR )
17 rexr 
 |-  ( w e. RR -> w e. RR* )
18 16 17 syl 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A /\ ( w + 1 ) <_ y ) -> w e. RR* )
19 1 rexrd 
 |-  ( w e. RR -> ( w + 1 ) e. RR* )
20 16 19 syl 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A /\ ( w + 1 ) <_ y ) -> ( w + 1 ) e. RR* )
21 simp1l 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A /\ ( w + 1 ) <_ y ) -> A C_ RR* )
22 simp2 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A /\ ( w + 1 ) <_ y ) -> y e. A )
23 ssel2 
 |-  ( ( A C_ RR* /\ y e. A ) -> y e. RR* )
24 21 22 23 syl2anc 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A /\ ( w + 1 ) <_ y ) -> y e. RR* )
25 16 ltp1d 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A /\ ( w + 1 ) <_ y ) -> w < ( w + 1 ) )
26 simp3 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A /\ ( w + 1 ) <_ y ) -> ( w + 1 ) <_ y )
27 18 20 24 25 26 xrltletrd 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A /\ ( w + 1 ) <_ y ) -> w < y )
28 27 3exp 
 |-  ( ( A C_ RR* /\ w e. RR ) -> ( y e. A -> ( ( w + 1 ) <_ y -> w < y ) ) )
29 28 adantlr 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A x <_ y ) /\ w e. RR ) -> ( y e. A -> ( ( w + 1 ) <_ y -> w < y ) ) )
30 15 29 reximdai 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A x <_ y ) /\ w e. RR ) -> ( E. y e. A ( w + 1 ) <_ y -> E. y e. A w < y ) )
31 8 30 mpd 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A x <_ y ) /\ w e. RR ) -> E. y e. A w < y )
32 31 ralrimiva 
 |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A x <_ y ) -> A. w e. RR E. y e. A w < y )
33 32 ex 
 |-  ( A C_ RR* -> ( A. x e. RR E. y e. A x <_ y -> A. w e. RR E. y e. A w < y ) )
34 breq1 
 |-  ( w = x -> ( w < y <-> x < y ) )
35 34 rexbidv 
 |-  ( w = x -> ( E. y e. A w < y <-> E. y e. A x < y ) )
36 35 cbvralvw 
 |-  ( A. w e. RR E. y e. A w < y <-> A. x e. RR E. y e. A x < y )
37 36 biimpi 
 |-  ( A. w e. RR E. y e. A w < y -> A. x e. RR E. y e. A x < y )
38 nfv 
 |-  F/ x A C_ RR*
39 nfra1 
 |-  F/ x A. x e. RR E. y e. A x < y
40 38 39 nfan 
 |-  F/ x ( A C_ RR* /\ A. x e. RR E. y e. A x < y )
41 simpll 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) /\ x e. RR ) -> A C_ RR* )
42 simpr 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) /\ x e. RR ) -> x e. RR )
43 rspa 
 |-  ( ( A. x e. RR E. y e. A x < y /\ x e. RR ) -> E. y e. A x < y )
44 43 adantll 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) /\ x e. RR ) -> E. y e. A x < y )
45 rexr 
 |-  ( x e. RR -> x e. RR* )
46 45 ad3antlr 
 |-  ( ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) /\ x < y ) -> x e. RR* )
47 23 adantr 
 |-  ( ( ( A C_ RR* /\ y e. A ) /\ x < y ) -> y e. RR* )
48 47 adantllr 
 |-  ( ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) /\ x < y ) -> y e. RR* )
49 simpr 
 |-  ( ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) /\ x < y ) -> x < y )
50 46 48 49 xrltled 
 |-  ( ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) /\ x < y ) -> x <_ y )
51 50 ex 
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) -> ( x < y -> x <_ y ) )
52 51 reximdva 
 |-  ( ( A C_ RR* /\ x e. RR ) -> ( E. y e. A x < y -> E. y e. A x <_ y ) )
53 52 adantlr 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) /\ x e. RR ) -> ( E. y e. A x < y -> E. y e. A x <_ y ) )
54 44 53 mpd 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) /\ x e. RR ) -> E. y e. A x <_ y )
55 simpr 
 |-  ( ( ( A C_ RR* /\ x e. RR ) /\ E. y e. A x <_ y ) -> E. y e. A x <_ y )
56 41 42 54 55 syl21anc 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) /\ x e. RR ) -> E. y e. A x <_ y )
57 56 ex 
 |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) -> ( x e. RR -> E. y e. A x <_ y ) )
58 40 57 ralrimi 
 |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A x < y ) -> A. x e. RR E. y e. A x <_ y )
59 37 58 sylan2 
 |-  ( ( A C_ RR* /\ A. w e. RR E. y e. A w < y ) -> A. x e. RR E. y e. A x <_ y )
60 59 ex 
 |-  ( A C_ RR* -> ( A. w e. RR E. y e. A w < y -> A. x e. RR E. y e. A x <_ y ) )
61 33 60 impbid 
 |-  ( A C_ RR* -> ( A. x e. RR E. y e. A x <_ y <-> A. w e. RR E. y e. A w < y ) )
62 supxrunb2 
 |-  ( A C_ RR* -> ( A. w e. RR E. y e. A w < y <-> sup ( A , RR* , < ) = +oo ) )
63 61 62 bitrd 
 |-  ( A C_ RR* -> ( A. x e. RR E. y e. A x <_ y <-> sup ( A , RR* , < ) = +oo ) )