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 ⁡ ℂ fld
lptioo2cn.2 ⊢ φ → A ∈ ℝ *
lptioo2cn.3 ⊢ φ → B ∈ ℝ
lptioo2cn.4 ⊢ φ → A < B
Assertion lptioo2cn ⊢ φ → B ∈ limPt ⁡ J ⁡ A B

Proof

Step Hyp Ref Expression
1 lptioo2cn.1 ⊢ J = TopOpen ⁡ ℂ fld
2 lptioo2cn.2 ⊢ φ → A ∈ ℝ *
3 lptioo2cn.3 ⊢ φ → B ∈ ℝ
4 lptioo2cn.4 ⊢ φ → A < B
5 eqid ⊢ topGen ⁡ ran ⁡ . = topGen ⁡ ran ⁡ .
6 5 2 3 4 lptioo2 ⊢ φ → B ∈ limPt ⁡ topGen ⁡ ran ⁡ . ⁡ A B
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 ⊢ A B ⊆ ℝ
13 eqid ⊢ ⋃ TopOpen ⁡ ℂ fld = ⋃ TopOpen ⁡ ℂ fld
14 7 tgioo2 ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
15 13 14 restlp ⊢ TopOpen ⁡ ℂ fld ∈ Top ∧ ℝ ⊆ ⋃ TopOpen ⁡ ℂ fld ∧ A B ⊆ ℝ → limPt ⁡ topGen ⁡ ran ⁡ . ⁡ A B = limPt ⁡ TopOpen ⁡ ℂ fld ⁡ A B ∩ ℝ
16 8 11 12 15 mp3an ⊢ limPt ⁡ topGen ⁡ ran ⁡ . ⁡ A B = limPt ⁡ TopOpen ⁡ ℂ fld ⁡ A B ∩ ℝ
17 6 16 eleqtrdi ⊢ φ → B ∈ limPt ⁡ TopOpen ⁡ ℂ fld ⁡ A B ∩ ℝ
18 elin ⊢ B ∈ limPt ⁡ TopOpen ⁡ ℂ fld ⁡ A B ∩ ℝ ↔ B ∈ limPt ⁡ TopOpen ⁡ ℂ fld ⁡ A B ∧ B ∈ ℝ
19 17 18 sylib ⊢ φ → B ∈ limPt ⁡ TopOpen ⁡ ℂ fld ⁡ A B ∧ B ∈ ℝ
20 19 simpld ⊢ φ → B ∈ limPt ⁡ TopOpen ⁡ ℂ fld ⁡ A B
21 1 eqcomi ⊢ TopOpen ⁡ ℂ fld = J
22 21 fveq2i ⊢ limPt ⁡ TopOpen ⁡ ℂ fld = limPt ⁡ J
23 22 fveq1i ⊢ limPt ⁡ TopOpen ⁡ ℂ fld ⁡ A B = limPt ⁡ J ⁡ A B
24 20 23 eleqtrdi ⊢ φ → B ∈ limPt ⁡ J ⁡ A B