hmeoclda

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

		Ref	Expression
	Assertion	hmeoclda	$⊢ ((J \in Top \land K \in Top \land F \in (J Homeo K)) \land S \in Clsd (J)) \to F [S] \in Clsd (K)$

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

Metamath Proof Explorer