hauscmp

Description: A compact subspace of a T2 space is closed. (Contributed by Jeff Hankins, 16-Jan-2010) (Proof shortened by Mario Carneiro, 14-Dec-2013)

		Ref	Expression
	Hypothesis	hauscmp.1	$⊢ X = ⋃ J$
	Assertion	hauscmp	$⊢ (J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \to S \in Clsd (J)$

Proof

Step	Hyp	Ref	Expression
1		hauscmp.1	$⊢ X = ⋃ J$
2		simp2	$⊢ (J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \to S \subseteq X$
3		eqid	$⊢ \{y \in J \| \exists w \in J (x \in w \land cls (J) (w) \subseteq X ∖ y)\} = \{y \in J \| \exists w \in J (x \in w \land cls (J) (w) \subseteq X ∖ y)\}$
4		simpl1	$⊢ ((J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \land x \in (X ∖ S)) \to J \in Haus$
5		simpl2	$⊢ ((J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \land x \in (X ∖ S)) \to S \subseteq X$
6		simpl3	$⊢ ((J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \land x \in (X ∖ S)) \to J ↾_{𝑡} S \in Comp$
7		simpr	$⊢ ((J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \land x \in (X ∖ S)) \to x \in (X ∖ S)$
8	1 3 4 5 6 7	hauscmplem	$⊢ ((J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \land x \in (X ∖ S)) \to \exists z \in J (x \in z \land cls (J) (z) \subseteq X ∖ S)$
9		haustop	$⊢ J \in Haus \to J \in Top$
10	9	3ad2ant1	$⊢ (J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \to J \in Top$
11		elssuni	$⊢ z \in J \to z \subseteq ⋃ J$
12	11 1	sseqtrrdi	$⊢ z \in J \to z \subseteq X$
13	1	sscls	$⊢ (J \in Top \land z \subseteq X) \to z \subseteq cls (J) (z)$
14	10 12 13	syl2an	$⊢ ((J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \land z \in J) \to z \subseteq cls (J) (z)$
15		sstr2	$⊢ z \subseteq cls (J) (z) \to (cls (J) (z) \subseteq X ∖ S \to z \subseteq X ∖ S)$
16	14 15	syl	$⊢ ((J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \land z \in J) \to (cls (J) (z) \subseteq X ∖ S \to z \subseteq X ∖ S)$
17	16	anim2d	$⊢ ((J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \land z \in J) \to ((x \in z \land cls (J) (z) \subseteq X ∖ S) \to (x \in z \land z \subseteq X ∖ S))$
18	17	reximdva	$⊢ (J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \to (\exists z \in J (x \in z \land cls (J) (z) \subseteq X ∖ S) \to \exists z \in J (x \in z \land z \subseteq X ∖ S))$
19	18	adantr	$⊢ ((J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \land x \in (X ∖ S)) \to (\exists z \in J (x \in z \land cls (J) (z) \subseteq X ∖ S) \to \exists z \in J (x \in z \land z \subseteq X ∖ S))$
20	8 19	mpd	$⊢ ((J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \land x \in (X ∖ S)) \to \exists z \in J (x \in z \land z \subseteq X ∖ S)$
21	20	ralrimiva	$⊢ (J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \to \forall x \in (X ∖ S) \exists z \in J (x \in z \land z \subseteq X ∖ S)$
22		eltop2	$⊢ J \in Top \to (X ∖ S \in J \leftrightarrow \forall x \in (X ∖ S) \exists z \in J (x \in z \land z \subseteq X ∖ S))$
23	10 22	syl	$⊢ (J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \to (X ∖ S \in J \leftrightarrow \forall x \in (X ∖ S) \exists z \in J (x \in z \land z \subseteq X ∖ S))$
24	21 23	mpbird	$⊢ (J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \to X ∖ S \in J$
25	1	iscld	$⊢ J \in Top \to (S \in Clsd (J) \leftrightarrow (S \subseteq X \land X ∖ S \in J))$
26	10 25	syl	$⊢ (J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \to (S \in Clsd (J) \leftrightarrow (S \subseteq X \land X ∖ S \in J))$
27	2 24 26	mpbir2and	$⊢ (J \in Haus \land S \subseteq X \land J ↾_{𝑡} S \in Comp) \to S \in Clsd (J)$

Metamath Proof Explorer

Theorem hauscmp

Proof