Metamath Proof Explorer

Theorem lptioo1cn

Description: The lower bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 lptioo1cn.1 
 |-  J = ( TopOpen ` CCfld )
2 lptioo1cn.2 
 |-  ( ph -> B e. RR* )
3 lptioo1cn.3 
 |-  ( ph -> A e. RR )
4 lptioo1cn.4 
 |-  ( ph -> A < B )
5 eqid 
 |-  ( topGen ` ran (,) ) = ( topGen ` ran (,) )
6 5 3 2 4 lptioo1 
 |-  ( ph -> A e. ( ( limPt ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
7 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
8 7 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
9 8 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. Top )
10 ax-resscn 
 |-  RR C_ CC
11 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
12 10 11 sseqtri 
 |-  RR C_ U. ( TopOpen ` CCfld )
13 12 a1i 
 |-  ( ph -> RR C_ U. ( TopOpen ` CCfld ) )
14 ioossre 
 |-  ( A (,) B ) C_ RR
15 14 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
16 eqid 
 |-  U. ( TopOpen ` CCfld ) = U. ( TopOpen ` CCfld )
17 7 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
18 16 17 restlp 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ RR C_ U. ( TopOpen ` CCfld ) /\ ( A (,) B ) C_ RR ) -> ( ( limPt ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A (,) B ) ) i^i RR ) )
19 9 13 15 18 syl3anc 
 |-  ( ph -> ( ( limPt ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A (,) B ) ) i^i RR ) )
20 6 19 eleqtrd 
 |-  ( ph -> A e. ( ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A (,) B ) ) i^i RR ) )
21 elin 
 |-  ( A e. ( ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A (,) B ) ) i^i RR ) <-> ( A e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A (,) B ) ) /\ A e. RR ) )
22 20 21 sylib 
 |-  ( ph -> ( A e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A (,) B ) ) /\ A e. RR ) )
23 22 simpld 
 |-  ( ph -> A e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A (,) B ) ) )
24 1 eqcomi 
 |-  ( TopOpen ` CCfld ) = J
25 24 fveq2i 
 |-  ( limPt ` ( TopOpen ` CCfld ) ) = ( limPt ` J )
26 25 fveq1i 
 |-  ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( A (,) B ) ) = ( ( limPt ` J ) ` ( A (,) B ) )
27 23 26 eleqtrdi 
 |-  ( ph -> A e. ( ( limPt ` J ) ` ( A (,) B ) ) )