Theorem rrxtopn0

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

	Ref	Expression
Assertion	rrxtopn0

Proof

Step	Hyp	Ref	Expression
1		0fin	$$⊢\varnothing \in \mathrm{Fin}$$
2		eqid
3	2	rrxtoponfi
4	1 3	ax-mp
5		reex	$$⊢ℝ\in \mathrm{V}$$
6		mapdm0	$$⊢ℝ\in \mathrm{V}\to {ℝ}^{\varnothing }=\left\{\varnothing \right\}$$
7	5 6	ax-mp	$$⊢{ℝ}^{\varnothing }=\left\{\varnothing \right\}$$
8	7	fveq2i	$$⊢\mathrm{TopOn}\left({ℝ}^{\varnothing }\right)=\mathrm{TopOn}\left(\left\{\varnothing \right\}\right)$$
9	4 8	eleqtri
10		topsn
11	9 10	ax-mp