Theorem hmphtop

Description: Reverse closure for the homeomorphic predicate. (Contributed by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Assertion	hmphtop	|- ( J ~= K -> ( J e. Top /\ K e. Top ) )

Proof

Step	Hyp	Ref	Expression
1		df-hmph	|- ~= = ( `' Homeo " ( _V \ 1o ) )
2		cnvimass	|- ( `' Homeo " ( _V \ 1o ) ) C_ dom Homeo
3		hmeofn	|- Homeo Fn ( Top X. Top )
4		fndm	|- ( Homeo Fn ( Top X. Top ) -> dom Homeo = ( Top X. Top ) )
5	3 4	ax-mp	|- dom Homeo = ( Top X. Top )
6	2 5	sseqtri	|- ( `' Homeo " ( _V \ 1o ) ) C_ ( Top X. Top )
7	1 6	eqsstri	|- ~= C_ ( Top X. Top )
8	7	brel	|- ( J ~= K -> ( J e. Top /\ K e. Top ) )