Theorem hmeoclda

Description: Homeomorphisms preserve closedness. (Contributed by Jeff Hankins, 3-Jul-2009) (Revised by Mario Carneiro, 3-Jun-2014)

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

Proof

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