Metamath Proof Explorer

Theorem rellycmp

Description: The topology on the reals is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion rellycmp 
|- ( topGen ` ran (,) ) e. N-Locally Comp

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
2 1 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
3 1 cnllycmp 
 |-  ( TopOpen ` CCfld ) e. N-Locally Comp
4 1 recld2 
 |-  RR e. ( Clsd ` ( TopOpen ` CCfld ) )
5 cldllycmp 
 |-  ( ( ( TopOpen ` CCfld ) e. N-Locally Comp /\ RR e. ( Clsd ` ( TopOpen ` CCfld ) ) ) -> ( ( TopOpen ` CCfld ) |`t RR ) e. N-Locally Comp )
6 3 4 5 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t RR ) e. N-Locally Comp
7 2 6 eqeltri 
 |-  ( topGen ` ran (,) ) e. N-Locally Comp