Theorem qqtopn

Description: The topology of the field of the rational numbers. (Contributed by Thierry Arnoux, 29-Aug-2020)

	Ref	Expression
Assertion	qqtopn	⊢ ( ( TopOpen ‘ ℝfld ) ↾t ℚ ) = ( TopOpen ‘ ( ℂfld ↾s ℚ ) )

Proof

Step	Hyp	Ref	Expression
1		retopn	⊢ ( topGen ‘ ran (,) ) = ( TopOpen ‘ ℝfld )
2	1	oveq1i	⊢ ( ( topGen ‘ ran (,) ) ↾t ℚ ) = ( ( TopOpen ‘ ℝfld ) ↾t ℚ )
3		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
4	3	oveq1i	⊢ ( ℝfld ↾s ℚ ) = ( ( ℂfld ↾s ℝ ) ↾s ℚ )
5		reex	⊢ ℝ ∈ V
6		qssre	⊢ ℚ ⊆ ℝ
7		ressabs	⊢ ( ( ℝ ∈ V ∧ ℚ ⊆ ℝ ) → ( ( ℂfld ↾s ℝ ) ↾s ℚ ) = ( ℂfld ↾s ℚ ) )
8	5 6 7	mp2an	⊢ ( ( ℂfld ↾s ℝ ) ↾s ℚ ) = ( ℂfld ↾s ℚ )
9	4 8	eqtr2i	⊢ ( ℂfld ↾s ℚ ) = ( ℝfld ↾s ℚ )
10	9 1	resstopn	⊢ ( ( topGen ‘ ran (,) ) ↾t ℚ ) = ( TopOpen ‘ ( ℂfld ↾s ℚ ) )
11	2 10	eqtr3i	⊢ ( ( TopOpen ‘ ℝfld ) ↾t ℚ ) = ( TopOpen ‘ ( ℂfld ↾s ℚ ) )