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 ≃ \{\emptyset\} \leftrightarrow J = \{\emptyset\}$

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

Metamath Proof Explorer