Theorem indistop

Description: The indiscrete topology on a set A . Part of Example 2 in Munkres p. 77. (Contributed by FL, 16-Jul-2006) (Revised by Stefan Allan, 6-Nov-2008) (Revised by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	indistop	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		indislem	$$⊢\left\{\varnothing ,\mathrm{I}\left(A\right)\right\}=\left\{\varnothing ,A\right\}$$
2		fvex	$$⊢\mathrm{I}\left(A\right)\in \mathrm{V}$$
3		indistopon	$$⊢\mathrm{I}\left(A\right)\in \mathrm{V}\to \left\{\varnothing ,\mathrm{I}\left(A\right)\right\}\in \mathrm{TopOn}\left(\mathrm{I}\left(A\right)\right)$$
4	2 3	ax-mp	$$⊢\left\{\varnothing ,\mathrm{I}\left(A\right)\right\}\in \mathrm{TopOn}\left(\mathrm{I}\left(A\right)\right)$$
5	4	topontopi	$$⊢\left\{\varnothing ,\mathrm{I}\left(A\right)\right\}\in \mathrm{Top}$$
6	1 5	eqeltrri	$$⊢\left\{\varnothing ,A\right\}\in \mathrm{Top}$$