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
|- ( (,) " ( QQ X. QQ ) ) e. TopBases

Proof

Step Hyp Ref Expression
1 qssre
 |-  QQ C_ RR
2 ressxr
 |-  RR C_ RR*
3 1 2 sstri
 |-  QQ C_ RR*
4 3 qtopbaslem
 |-  ( (,) " ( QQ X. QQ ) ) e. TopBases