Theorem hmphtop

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

	Ref	Expression
Assertion	hmphtop	⊢ ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) )

Proof

Step	Hyp	Ref	Expression
1		df-hmph	⊢ ≃ = ( ◡ Homeo “ ( V ∖ 1o ) )
2		cnvimass	⊢ ( ◡ Homeo “ ( V ∖ 1o ) ) ⊆ dom Homeo
3		hmeofn	⊢ Homeo Fn ( Top × Top )
4		fndm	⊢ ( Homeo Fn ( Top × Top ) → dom Homeo = ( Top × Top ) )
5	3 4	ax-mp	⊢ dom Homeo = ( Top × Top )
6	2 5	sseqtri	⊢ ( ◡ Homeo “ ( V ∖ 1o ) ) ⊆ ( Top × Top )
7	1 6	eqsstri	⊢ ≃ ⊆ ( Top × Top )
8	7	brel	⊢ ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) )