Theorem hmph

Description: Express the predicate J is homeomorphic to K . (Contributed by FL, 14-Feb-2007) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Assertion	hmph	⊢ ( 𝐽 ≃ 𝐾 ↔ ( 𝐽 Homeo 𝐾 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-hmph	⊢ ≃ = ( ◡ Homeo “ ( V ∖ 1o ) )
2		hmeofn	⊢ Homeo Fn ( Top × Top )
3	1 2	brwitnlem	⊢ ( 𝐽 ≃ 𝐾 ↔ ( 𝐽 Homeo 𝐾 ) ≠ ∅ )