Theorem rrxtopn0

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

	Ref	Expression
Assertion	rrxtopn0	⊢ ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) = 𝒫 { ∅ }

Proof

Step	Hyp	Ref	Expression
1		0fin	⊢ ∅ ∈ Fin
2		eqid	⊢ ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) = ( TopOpen ‘ ( ℝ^ ‘ ∅ ) )
3	2	rrxtoponfi	⊢ ( ∅ ∈ Fin → ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) ∈ ( TopOn ‘ ( ℝ ↑m ∅ ) ) )
4	1 3	ax-mp	⊢ ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) ∈ ( TopOn ‘ ( ℝ ↑m ∅ ) )
5		reex	⊢ ℝ ∈ V
6		mapdm0	⊢ ( ℝ ∈ V → ( ℝ ↑m ∅ ) = { ∅ } )
7	5 6	ax-mp	⊢ ( ℝ ↑m ∅ ) = { ∅ }
8	7	fveq2i	⊢ ( TopOn ‘ ( ℝ ↑m ∅ ) ) = ( TopOn ‘ { ∅ } )
9	4 8	eleqtri	⊢ ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) ∈ ( TopOn ‘ { ∅ } )
10		topsn	⊢ ( ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) ∈ ( TopOn ‘ { ∅ } ) → ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) = 𝒫 { ∅ } )
11	9 10	ax-mp	⊢ ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) = 𝒫 { ∅ }