Theorem hmphtop1

Description: The relation "being homeomorphic to" implies the operands are topologies. (Contributed by FL, 23-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		hmphtop	⊢ ( 𝐽 ≃ 𝐾 → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) )
2	1	simpld	⊢ ( 𝐽 ≃ 𝐾 → 𝐽 ∈ Top )