tgioo3

Description: The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014) (Revised by Thierry Arnoux, 3-Jul-2019)

		Ref	Expression
	Hypothesis	tgioo3.1	$⊢ J = TopOpen (ℝ_{fld})$
	Assertion	tgioo3	$⊢ topGen (ran (.)) = J$

Proof

Step	Hyp	Ref	Expression
1		tgioo3.1	$⊢ J = TopOpen (ℝ_{fld})$
2		eqid	$⊢ ℂ_{fld} ↾_{𝑠} ℝ = ℂ_{fld} ↾_{𝑠} ℝ$
3		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
4	2 3	resstopn	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ = TopOpen (ℂ_{fld} ↾_{𝑠} ℝ)$
5		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
6		df-refld	$⊢ ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$
7	6	fveq2i	$⊢ TopOpen (ℝ_{fld}) = TopOpen (ℂ_{fld} ↾_{𝑠} ℝ)$
8	1 7	eqtri	$⊢ J = TopOpen (ℂ_{fld} ↾_{𝑠} ℝ)$
9	4 5 8	3eqtr4i	$⊢ topGen (ran (.)) = J$

Metamath Proof Explorer

Theorem tgioo3

Proof