Metamath Proof Explorer

Theorem hmeocldb

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

		Ref	Expression
	Assertion	hmeocldb	$⊢ ((J \in Top \land K \in Top \land F \in (J Homeo K)) \land S \in Clsd (K)) \to F^{-1} [S] \in Clsd (J)$

Step	Hyp	Ref	Expression
1		hmeocn	$⊢ F \in (J Homeo K) \to F \in (J Cn K)$
2	1	3ad2ant3	$⊢ (J \in Top \land K \in Top \land F \in (J Homeo K)) \to F \in (J Cn K)$
3		cnclima	$⊢ (F \in (J Cn K) \land S \in Clsd (K)) \to F^{-1} [S] \in Clsd (J)$
4	2 3	sylan	$⊢ ((J \in Top \land K \in Top \land F \in (J Homeo K)) \land S \in Clsd (K)) \to F^{-1} [S] \in Clsd (J)$