Metamath Proof Explorer

Theorem reordt

Description: The real numbers are an open set in the topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion reordt 
|- RR e. ( ordTop ` <_ )

Proof

Step Hyp Ref Expression
1 ioomax 
 |-  ( -oo (,) +oo ) = RR
2 iooordt 
 |-  ( -oo (,) +oo ) e. ( ordTop ` <_ )
3 1 2 eqeltrri 
 |-  RR e. ( ordTop ` <_ )