Theorem rrxtopn0b

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

	Ref	Expression
Assertion	rrxtopn0b	⊢ ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) = { ∅ , { ∅ } }

Proof

Step	Hyp	Ref	Expression
1		rrxtopn0	⊢ ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) = 𝒫 { ∅ }
2		pwsn	⊢ 𝒫 { ∅ } = { ∅ , { ∅ } }
3	1 2	eqtri	⊢ ( TopOpen ‘ ( ℝ^ ‘ ∅ ) ) = { ∅ , { ∅ } }