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 𝐽 = ( TopOpen ‘ ℂfld )
lptioo2cn.2 ( 𝜑𝐴 ∈ ℝ* )
lptioo2cn.3 ( 𝜑𝐵 ∈ ℝ )
lptioo2cn.4 ( 𝜑𝐴 < 𝐵 )
Assertion lptioo2cn ( 𝜑𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 (,) 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 lptioo2cn.1 𝐽 = ( TopOpen ‘ ℂfld )
2 lptioo2cn.2 ( 𝜑𝐴 ∈ ℝ* )
3 lptioo2cn.3 ( 𝜑𝐵 ∈ ℝ )
4 lptioo2cn.4 ( 𝜑𝐴 < 𝐵 )
5 eqid ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
6 5 2 3 4 lptioo2 ( 𝜑𝐵 ∈ ( ( limPt ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
7 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
8 7 cnfldtop ( TopOpen ‘ ℂfld ) ∈ Top
9 ax-resscn ℝ ⊆ ℂ
10 unicntop ℂ = ( TopOpen ‘ ℂfld )
11 9 10 sseqtri ℝ ⊆ ( TopOpen ‘ ℂfld )
12 ioossre ( 𝐴 (,) 𝐵 ) ⊆ ℝ
13 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
14 7 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
15 13 14 restlp ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ℝ ⊆ ( TopOpen ‘ ℂfld ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ ) → ( ( limPt ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ∩ ℝ ) )
16 8 11 12 15 mp3an ( ( limPt ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ∩ ℝ )
17 6 16 eleqtrdi ( 𝜑𝐵 ∈ ( ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ∩ ℝ ) )
18 elin ( 𝐵 ∈ ( ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ∩ ℝ ) ↔ ( 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ∧ 𝐵 ∈ ℝ ) )
19 17 18 sylib ( 𝜑 → ( 𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 (,) 𝐵 ) ) ∧ 𝐵 ∈ ℝ ) )
20 19 simpld ( 𝜑𝐵 ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 (,) 𝐵 ) ) )
21 1 eqcomi ( TopOpen ‘ ℂfld ) = 𝐽
22 21 fveq2i ( limPt ‘ ( TopOpen ‘ ℂfld ) ) = ( limPt ‘ 𝐽 )
23 22 fveq1i ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( 𝐴 (,) 𝐵 ) ) = ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 (,) 𝐵 ) )
24 20 23 eleqtrdi ( 𝜑𝐵 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( 𝐴 (,) 𝐵 ) ) )