Theorem hmphsym

Description: "Is homeomorphic to" is symmetric. (Contributed by FL, 8-Mar-2007) (Proof shortened by Mario Carneiro, 30-May-2014)

	Ref	Expression
Assertion	hmphsym	⊢ ( 𝐽 ≃ 𝐾 → 𝐾 ≃ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		hmph	⊢ ( 𝐽 ≃ 𝐾 ↔ ( 𝐽 Homeo 𝐾 ) ≠ ∅ )
2		n0	⊢ ( ( 𝐽 Homeo 𝐾 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) )
3	1 2	bitri	⊢ ( 𝐽 ≃ 𝐾 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) )
4		hmeocnv	⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝑓 ∈ ( 𝐾 Homeo 𝐽 ) )
5		hmphi	⊢ ( ◡ 𝑓 ∈ ( 𝐾 Homeo 𝐽 ) → 𝐾 ≃ 𝐽 )
6	4 5	syl	⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐾 ≃ 𝐽 )
7	6	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐾 ≃ 𝐽 )
8	3 7	sylbi	⊢ ( 𝐽 ≃ 𝐾 → 𝐾 ≃ 𝐽 )