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

Proof

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