Metamath Proof Explorer

Theorem lptioo2cn

Description: The upper 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 lptioo2cn.1 
|- J = ( TopOpen ` CCfld )
lptioo2cn.2 
|- ( ph -> A e. RR* )
lptioo2cn.3 
|- ( ph -> B e. RR )
lptioo2cn.4 
|- ( ph -> A < B )
Assertion lptioo2cn 
|- ( ph -> B e. ( ( limPt ` J ) ` ( A (,) B ) ) )

Proof

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