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	$⊢ φ \to A \in ℝ^{*}$
	lptioo2cn.3	$⊢ φ \to B \in ℝ$
	lptioo2cn.4	$⊢ φ \to A < B$
Assertion	lptioo2cn	$⊢ φ \to B \in limPt (J) ((A, B))$

Proof

Step	Hyp	Ref	Expression
1		lptioo2cn.1	$⊢ J = TopOpen (ℂ_{fld})$
2		lptioo2cn.2	$⊢ φ \to A \in ℝ^{*}$
3		lptioo2cn.3	$⊢ φ \to B \in ℝ$
4		lptioo2cn.4	$⊢ φ \to A < B$
5		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
6	5 2 3 4	lptioo2	$⊢ φ \to B \in limPt (topGen (ran (.))) ((A, B))$
7		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
8	7	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
9		ax-resscn	$⊢ ℝ \subseteq ℂ$
10		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
11	9 10	sseqtri	$⊢ ℝ \subseteq ⋃ TopOpen (ℂ_{fld})$
12		ioossre	$⊢ (A, B) \subseteq ℝ$
13		eqid	$⊢ ⋃ TopOpen (ℂ_{fld}) = ⋃ TopOpen (ℂ_{fld})$
14	7	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
15	13 14	restlp	$⊢ (TopOpen (ℂ_{fld}) \in Top \land ℝ \subseteq ⋃ TopOpen (ℂ_{fld}) \land (A, B) \subseteq ℝ) \to limPt (topGen (ran (.))) ((A, B)) = limPt (TopOpen (ℂ_{fld})) ((A, B)) \cap ℝ$
16	8 11 12 15	mp3an	$⊢ limPt (topGen (ran (.))) ((A, B)) = limPt (TopOpen (ℂ_{fld})) ((A, B)) \cap ℝ$
17	6 16	eleqtrdi	$⊢ φ \to B \in (limPt (TopOpen (ℂ_{fld})) ((A, B)) \cap ℝ)$
18		elin	$⊢ B \in (limPt (TopOpen (ℂ_{fld})) ((A, B)) \cap ℝ) \leftrightarrow (B \in limPt (TopOpen (ℂ_{fld})) ((A, B)) \land B \in ℝ)$
19	17 18	sylib	$⊢ φ \to (B \in limPt (TopOpen (ℂ_{fld})) ((A, B)) \land B \in ℝ)$
20	19	simpld	$⊢ φ \to B \in 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	$⊢ φ \to B \in limPt (J) ((A, B))$

Metamath Proof Explorer

Theorem lptioo2cn

Proof