Metamath Proof Explorer

Theorem rrxtopn0b

Description: The topology of the zero-dimensional real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Assertion rrxtopn0b 
|- ( TopOpen ` ( RR^ ` (/) ) ) = { (/) , { (/) } }

Proof

Step Hyp Ref Expression
1 rrxtopn0 
 |-  ( TopOpen ` ( RR^ ` (/) ) ) = ~P { (/) }
2 pwsn 
 |-  ~P { (/) } = { (/) , { (/) } }
3 1 2 eqtri 
 |-  ( TopOpen ` ( RR^ ` (/) ) ) = { (/) , { (/) } }