This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐽 ) ) )