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 tgioo4 ⊢ ( 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 ‘ 𝐽 ) ‘ ( 𝐴 (,) 𝐵 ) ) )