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 ~= { (/) } <-> J = { (/) } )

Proof

Step	Hyp	Ref	Expression
1		hmphen	|- ( J ~= { (/) } -> J ~~ { (/) } )
2		df1o2	|- 1o = { (/) }
3	1 2	breqtrrdi	|- ( J ~= { (/) } -> J ~~ 1o )
4		hmphtop1	|- ( J ~= { (/) } -> J e. Top )
5		en1top	|- ( J e. Top -> ( J ~~ 1o <-> J = { (/) } ) )
6	4 5	syl	|- ( J ~= { (/) } -> ( J ~~ 1o <-> J = { (/) } ) )
7	3 6	mpbid	|- ( J ~= { (/) } -> J = { (/) } )
8		id	|- ( J = { (/) } -> J = { (/) } )
9		sn0top	|- { (/) } e. Top
10		hmphref	|- ( { (/) } e. Top -> { (/) } ~= { (/) } )
11	9 10	ax-mp	|- { (/) } ~= { (/) }
12	8 11	eqbrtrdi	|- ( J = { (/) } -> J ~= { (/) } )
13	7 12	impbii	|- ( J ~= { (/) } <-> J = { (/) } )