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