hmphtop

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

		Ref	Expression
	Assertion	hmphtop	$⊢ J ≃ K \to (J \in Top \land K \in Top)$

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

Metamath Proof Explorer