Metamath Proof Explorer

Theorem lptioo2

Description: The upper bound of an open interval is a limit point of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses lptioo2.1 
|- J = ( topGen ` ran (,) )
lptioo2.2 
|- ( ph -> A e. RR* )
lptioo2.3 
|- ( ph -> B e. RR )
lptioo2.4 
|- ( ph -> A < B )
Assertion lptioo2 
|- ( ph -> B e. ( ( limPt ` J ) ` ( A (,) B ) ) )

Proof

Step Hyp Ref Expression
1 lptioo2.1 
 |-  J = ( topGen ` ran (,) )
2 lptioo2.2 
 |-  ( ph -> A e. RR* )
3 lptioo2.3 
 |-  ( ph -> B e. RR )
4 lptioo2.4 
 |-  ( ph -> A < B )
5 difssd 
 |-  ( ph -> ( ( A (,) B ) \ { B } ) C_ ( A (,) B ) )
6 simpr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A (,) B ) )
7 ubioo 
 |-  -. B e. ( A (,) B )
8 eleq1 
 |-  ( x = B -> ( x e. ( A (,) B ) <-> B e. ( A (,) B ) ) )
9 8 biimpcd 
 |-  ( x e. ( A (,) B ) -> ( x = B -> B e. ( A (,) B ) ) )
10 7 9 mtoi 
 |-  ( x e. ( A (,) B ) -> -. x = B )
11 10 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -. x = B )
12 velsn 
 |-  ( x e. { B } <-> x = B )
13 11 12 sylnibr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -. x e. { B } )
14 6 13 eldifd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( ( A (,) B ) \ { B } ) )
15 5 14 eqelssd 
 |-  ( ph -> ( ( A (,) B ) \ { B } ) = ( A (,) B ) )
16 15 ineq2d 
 |-  ( ph -> ( ( a (,) b ) i^i ( ( A (,) B ) \ { B } ) ) = ( ( a (,) b ) i^i ( A (,) B ) ) )
17 16 ad2antrr 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> ( ( a (,) b ) i^i ( ( A (,) B ) \ { B } ) ) = ( ( a (,) b ) i^i ( A (,) B ) ) )
18 simplrl 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> a e. RR* )
19 simplrr 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> b e. RR* )
20 2 ad2antrr 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> A e. RR* )
21 elioo3g 
 |-  ( B e. ( a (,) b ) <-> ( ( a e. RR* /\ b e. RR* /\ B e. RR* ) /\ ( a < B /\ B < b ) ) )
22 21 biimpi 
 |-  ( B e. ( a (,) b ) -> ( ( a e. RR* /\ b e. RR* /\ B e. RR* ) /\ ( a < B /\ B < b ) ) )
23 22 simpld 
 |-  ( B e. ( a (,) b ) -> ( a e. RR* /\ b e. RR* /\ B e. RR* ) )
24 23 simp3d 
 |-  ( B e. ( a (,) b ) -> B e. RR* )
25 24 adantl 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> B e. RR* )
26 iooin 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ ( A e. RR* /\ B e. RR* ) ) -> ( ( a (,) b ) i^i ( A (,) B ) ) = ( if ( a <_ A , A , a ) (,) if ( b <_ B , b , B ) ) )
27 18 19 20 25 26 syl22anc 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> ( ( a (,) b ) i^i ( A (,) B ) ) = ( if ( a <_ A , A , a ) (,) if ( b <_ B , b , B ) ) )
28 iftrue 
 |-  ( a <_ A -> if ( a <_ A , A , a ) = A )
29 28 adantl 
 |-  ( ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) /\ a <_ A ) -> if ( a <_ A , A , a ) = A )
30 4 ad3antrrr 
 |-  ( ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) /\ a <_ A ) -> A < B )
31 29 30 eqbrtrd 
 |-  ( ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) /\ a <_ A ) -> if ( a <_ A , A , a ) < B )
32 iffalse 
 |-  ( -. a <_ A -> if ( a <_ A , A , a ) = a )
33 32 adantl 
 |-  ( ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) /\ -. a <_ A ) -> if ( a <_ A , A , a ) = a )
34 22 simprd 
 |-  ( B e. ( a (,) b ) -> ( a < B /\ B < b ) )
35 34 simpld 
 |-  ( B e. ( a (,) b ) -> a < B )
36 35 ad2antlr 
 |-  ( ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) /\ -. a <_ A ) -> a < B )
37 33 36 eqbrtrd 
 |-  ( ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) /\ -. a <_ A ) -> if ( a <_ A , A , a ) < B )
38 31 37 pm2.61dan 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> if ( a <_ A , A , a ) < B )
39 34 simprd 
 |-  ( B e. ( a (,) b ) -> B < b )
40 23 simp2d 
 |-  ( B e. ( a (,) b ) -> b e. RR* )
41 xrltnle 
 |-  ( ( B e. RR* /\ b e. RR* ) -> ( B < b <-> -. b <_ B ) )
42 24 40 41 syl2anc 
 |-  ( B e. ( a (,) b ) -> ( B < b <-> -. b <_ B ) )
43 39 42 mpbid 
 |-  ( B e. ( a (,) b ) -> -. b <_ B )
44 iffalse 
 |-  ( -. b <_ B -> if ( b <_ B , b , B ) = B )
45 43 44 syl 
 |-  ( B e. ( a (,) b ) -> if ( b <_ B , b , B ) = B )
46 45 eqcomd 
 |-  ( B e. ( a (,) b ) -> B = if ( b <_ B , b , B ) )
47 46 adantl 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> B = if ( b <_ B , b , B ) )
48 38 47 breqtrd 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> if ( a <_ A , A , a ) < if ( b <_ B , b , B ) )
49 20 18 ifcld 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> if ( a <_ A , A , a ) e. RR* )
50 47 25 eqeltrrd 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> if ( b <_ B , b , B ) e. RR* )
51 ioon0 
 |-  ( ( if ( a <_ A , A , a ) e. RR* /\ if ( b <_ B , b , B ) e. RR* ) -> ( ( if ( a <_ A , A , a ) (,) if ( b <_ B , b , B ) ) =/= (/) <-> if ( a <_ A , A , a ) < if ( b <_ B , b , B ) ) )
52 49 50 51 syl2anc 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> ( ( if ( a <_ A , A , a ) (,) if ( b <_ B , b , B ) ) =/= (/) <-> if ( a <_ A , A , a ) < if ( b <_ B , b , B ) ) )
53 48 52 mpbird 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> ( if ( a <_ A , A , a ) (,) if ( b <_ B , b , B ) ) =/= (/) )
54 27 53 eqnetrd 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> ( ( a (,) b ) i^i ( A (,) B ) ) =/= (/) )
55 17 54 eqnetrd 
 |-  ( ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) /\ B e. ( a (,) b ) ) -> ( ( a (,) b ) i^i ( ( A (,) B ) \ { B } ) ) =/= (/) )
56 55 ex 
 |-  ( ( ph /\ ( a e. RR* /\ b e. RR* ) ) -> ( B e. ( a (,) b ) -> ( ( a (,) b ) i^i ( ( A (,) B ) \ { B } ) ) =/= (/) ) )
57 56 ralrimivva 
 |-  ( ph -> A. a e. RR* A. b e. RR* ( B e. ( a (,) b ) -> ( ( a (,) b ) i^i ( ( A (,) B ) \ { B } ) ) =/= (/) ) )
58 ioossre 
 |-  ( A (,) B ) C_ RR
59 58 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
60 1 59 3 islptre 
 |-  ( ph -> ( B e. ( ( limPt ` J ) ` ( A (,) B ) ) <-> A. a e. RR* A. b e. RR* ( B e. ( a (,) b ) -> ( ( a (,) b ) i^i ( ( A (,) B ) \ { B } ) ) =/= (/) ) ) )
61 57 60 mpbird 
 |-  ( ph -> B e. ( ( limPt ` J ) ` ( A (,) B ) ) )