Theorem hmphtop

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

	Ref	Expression
Assertion	hmphtop	$$⊢J\simeq K\to \left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-hmph	$$⊢\simeq ={\mathrm{Homeo}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
2		cnvimass	$$⊢{\mathrm{Homeo}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]\subseteq \mathrm{dom}\mathrm{Homeo}$$
3		hmeofn	$$⊢\mathrm{Homeo}Fn\left(\mathrm{Top}\times \mathrm{Top}\right)$$
4		fndm	$$⊢\mathrm{Homeo}Fn\left(\mathrm{Top}\times \mathrm{Top}\right)\to \mathrm{dom}\mathrm{Homeo}=\mathrm{Top}\times \mathrm{Top}$$
5	3 4	ax-mp	$$⊢\mathrm{dom}\mathrm{Homeo}=\mathrm{Top}\times \mathrm{Top}$$
6	2 5	sseqtri	$$⊢{\mathrm{Homeo}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]\subseteq \mathrm{Top}\times \mathrm{Top}$$
7	1 6	eqsstri	$$⊢\simeq \subseteq \mathrm{Top}\times \mathrm{Top}$$
8	7	brel	$$⊢J\simeq K\to \left(J\in \mathrm{Top}\wedge K\in \mathrm{Top}\right)$$