Theorem hmeocnv

Description: The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Assertion	hmeocnv	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Homeo 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		hmeocnvcn	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) )
2		hmeocn	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
4		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
5	3 4	cnf	⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 )
6		frel	⊢ ( 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 → Rel 𝐹 )
7	2 5 6	3syl	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → Rel 𝐹 )
8		dfrel2	⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 )
9	7 8	sylib	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ ◡ 𝐹 = 𝐹 )
10	9 2	eqeltrd	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ ◡ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
11		ishmeo	⊢ ( ◡ 𝐹 ∈ ( 𝐾 Homeo 𝐽 ) ↔ ( ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ∧ ◡ ◡ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) )
12	1 10 11	sylanbrc	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → ◡ 𝐹 ∈ ( 𝐾 Homeo 𝐽 ) )