Theorem hmeocldb

Description: Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009)

	Ref	Expression
Assertion	hmeocldb	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		hmeocn	⊢ ( 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
2	1	3ad2ant3	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3		cnclima	⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )
4	2 3	sylan	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ( 𝐽 Homeo 𝐾 ) ) ∧ 𝑆 ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )