Theorem indislem

Description: A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	indislem	$$⊢\left\{\varnothing ,\mathrm{I}\left(A\right)\right\}=\left\{\varnothing ,A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fvi	$$⊢A\in \mathrm{V}\to \mathrm{I}\left(A\right)=A$$
2	1	preq2d	$$⊢A\in \mathrm{V}\to \left\{\varnothing ,\mathrm{I}\left(A\right)\right\}=\left\{\varnothing ,A\right\}$$
3		dfsn2	$$⊢\left\{\varnothing \right\}=\left\{\varnothing ,\varnothing \right\}$$
4	3	eqcomi	$$⊢\left\{\varnothing ,\varnothing \right\}=\left\{\varnothing \right\}$$
5		fvprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{I}\left(A\right)=\varnothing$$
6	5	preq2d	$$⊢\neg A\in \mathrm{V}\to \left\{\varnothing ,\mathrm{I}\left(A\right)\right\}=\left\{\varnothing ,\varnothing \right\}$$
7		prprc2	$$⊢\neg A\in \mathrm{V}\to \left\{\varnothing ,A\right\}=\left\{\varnothing \right\}$$
8	4 6 7	3eqtr4a	$$⊢\neg A\in \mathrm{V}\to \left\{\varnothing ,\mathrm{I}\left(A\right)\right\}=\left\{\varnothing ,A\right\}$$
9	2 8	pm2.61i	$$⊢\left\{\varnothing ,\mathrm{I}\left(A\right)\right\}=\left\{\varnothing ,A\right\}$$