Metamath Proof Explorer

Theorem rrxtopn0

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

Ref Expression
Assertion rrxtopn0 
|- ( TopOpen ` ( RR^ ` (/) ) ) = ~P { (/) }

Proof

Step Hyp Ref Expression
1 0fin 
 |-  (/) e. Fin
2 eqid 
 |-  ( TopOpen ` ( RR^ ` (/) ) ) = ( TopOpen ` ( RR^ ` (/) ) )
3 2 rrxtoponfi 
 |-  ( (/) e. Fin -> ( TopOpen ` ( RR^ ` (/) ) ) e. ( TopOn ` ( RR ^m (/) ) ) )
4 1 3 ax-mp 
 |-  ( TopOpen ` ( RR^ ` (/) ) ) e. ( TopOn ` ( RR ^m (/) ) )
5 reex 
 |-  RR e. _V
6 mapdm0 
 |-  ( RR e. _V -> ( RR ^m (/) ) = { (/) } )
7 5 6 ax-mp 
 |-  ( RR ^m (/) ) = { (/) }
8 7 fveq2i 
 |-  ( TopOn ` ( RR ^m (/) ) ) = ( TopOn ` { (/) } )
9 4 8 eleqtri 
 |-  ( TopOpen ` ( RR^ ` (/) ) ) e. ( TopOn ` { (/) } )
10 topsn 
 |-  ( ( TopOpen ` ( RR^ ` (/) ) ) e. ( TopOn ` { (/) } ) -> ( TopOpen ` ( RR^ ` (/) ) ) = ~P { (/) } )
11 9 10 ax-mp 
 |-  ( TopOpen ` ( RR^ ` (/) ) ) = ~P { (/) }