Theorem hmph0

Description: A topology homeomorphic to the empty set is empty. (Contributed by FL, 18-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Assertion	hmph0	$$⊢J\simeq \left\{\varnothing \right\}\leftrightarrow J=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		hmphen	$$⊢J\simeq \left\{\varnothing \right\}\to J\approx \left\{\varnothing \right\}$$
2		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
3	1 2	breqtrrdi	$$⊢J\simeq \left\{\varnothing \right\}\to J\approx 1_{𝑜}$$
4		hmphtop1	$$⊢J\simeq \left\{\varnothing \right\}\to J\in \mathrm{Top}$$
5		en1top	$$⊢J\in \mathrm{Top}\to \left(J\approx 1_{𝑜}\leftrightarrow J=\left\{\varnothing \right\}\right)$$
6	4 5	syl	$$⊢J\simeq \left\{\varnothing \right\}\to \left(J\approx 1_{𝑜}\leftrightarrow J=\left\{\varnothing \right\}\right)$$
7	3 6	mpbid	$$⊢J\simeq \left\{\varnothing \right\}\to J=\left\{\varnothing \right\}$$
8		id	$$⊢J=\left\{\varnothing \right\}\to J=\left\{\varnothing \right\}$$
9		sn0top	$$⊢\left\{\varnothing \right\}\in \mathrm{Top}$$
10		hmphref	$$⊢\left\{\varnothing \right\}\in \mathrm{Top}\to \left\{\varnothing \right\}\simeq \left\{\varnothing \right\}$$
11	9 10	ax-mp	$$⊢\left\{\varnothing \right\}\simeq \left\{\varnothing \right\}$$
12	8 11	eqbrtrdi	$$⊢J=\left\{\varnothing \right\}\to J\simeq \left\{\varnothing \right\}$$
13	7 12	impbii	$$⊢J\simeq \left\{\varnothing \right\}\leftrightarrow J=\left\{\varnothing \right\}$$