Metamath Proof Explorer

Theorem lptioo1

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

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

Proof

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