Theorem ishmeo

Description: The predicate F is a homeomorphism between topology J and topology K . Criterion of BourbakiTop1 p. I.2. (Contributed by FL, 14-Feb-2007) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Assertion	ishmeo	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ↔ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnveq	⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 )
2	1	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) ↔ ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ) )
3		hmeofval	⊢ ( 𝐽 Homeo 𝐾 ) = { 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∣ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) }
4	2 3	elrab2	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ↔ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ◡ 𝐹 ∈ ( 𝐾 Cn 𝐽 ) ) )