This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qtopbas

Description: The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007)

		Ref	Expression
	Assertion	qtopbas	$⊢ (.) [ℚ \times ℚ] \in TopBases$

Step	Hyp	Ref	Expression
1		qssre	$⊢ ℚ \subseteq ℝ$
2		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
3	1 2	sstri	$⊢ ℚ \subseteq ℝ^{*}$
4	3	qtopbaslem	$⊢ (.) [ℚ \times ℚ] \in TopBases$