hausllycmp

Description: A compact Hausdorff space is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	hausllycmp	$⊢ (J \in Haus \land J \in Comp) \to J \in N-LocallyComp$

Proof

Step	Hyp	Ref	Expression
1		haustop	$⊢ J \in Haus \to J \in Top$
2	1	adantr	$⊢ (J \in Haus \land J \in Comp) \to J \in Top$
3		eqid	$⊢ ⋃ J = ⋃ J$
4		eqid	$⊢ \{z \in J \| \exists v \in J (y \in v \land cls (J) (v) \subseteq ⋃ J ∖ z)\} = \{z \in J \| \exists v \in J (y \in v \land cls (J) (v) \subseteq ⋃ J ∖ z)\}$
5		simpll	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to J \in Haus$
6		difssd	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to ⋃ J ∖ x \subseteq ⋃ J$
7		simplr	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to J \in Comp$
8	1	ad2antrr	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to J \in Top$
9		simprl	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to x \in J$
10	3	opncld	$⊢ (J \in Top \land x \in J) \to ⋃ J ∖ x \in Clsd (J)$
11	8 9 10	syl2anc	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to ⋃ J ∖ x \in Clsd (J)$
12		cmpcld	$⊢ (J \in Comp \land ⋃ J ∖ x \in Clsd (J)) \to J ↾_{𝑡} (⋃ J ∖ x) \in Comp$
13	7 11 12	syl2anc	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to J ↾_{𝑡} (⋃ J ∖ x) \in Comp$
14		simprr	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to y \in x$
15		elssuni	$⊢ x \in J \to x \subseteq ⋃ J$
16	15	ad2antrl	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to x \subseteq ⋃ J$
17		dfss4	$⊢ x \subseteq ⋃ J \leftrightarrow ⋃ J ∖ (⋃ J ∖ x) = x$
18	16 17	sylib	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to ⋃ J ∖ (⋃ J ∖ x) = x$
19	14 18	eleqtrrd	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to y \in (⋃ J ∖ (⋃ J ∖ x))$
20	3 4 5 6 13 19	hauscmplem	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to \exists u \in J (y \in u \land cls (J) (u) \subseteq ⋃ J ∖ (⋃ J ∖ x))$
21	18	sseq2d	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to (cls (J) (u) \subseteq ⋃ J ∖ (⋃ J ∖ x) \leftrightarrow cls (J) (u) \subseteq x)$
22	21	anbi2d	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to ((y \in u \land cls (J) (u) \subseteq ⋃ J ∖ (⋃ J ∖ x)) \leftrightarrow (y \in u \land cls (J) (u) \subseteq x))$
23	22	rexbidv	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to (\exists u \in J (y \in u \land cls (J) (u) \subseteq ⋃ J ∖ (⋃ J ∖ x)) \leftrightarrow \exists u \in J (y \in u \land cls (J) (u) \subseteq x))$
24	20 23	mpbid	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to \exists u \in J (y \in u \land cls (J) (u) \subseteq x)$
25	8	adantr	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to J \in Top$
26		simprl	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to u \in J$
27		simprrl	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to y \in u$
28		opnneip	$⊢ (J \in Top \land u \in J \land y \in u) \to u \in nei (J) (\{y\})$
29	25 26 27 28	syl3anc	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to u \in nei (J) (\{y\})$
30		elssuni	$⊢ u \in J \to u \subseteq ⋃ J$
31	30	ad2antrl	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to u \subseteq ⋃ J$
32	3	sscls	$⊢ (J \in Top \land u \subseteq ⋃ J) \to u \subseteq cls (J) (u)$
33	25 31 32	syl2anc	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to u \subseteq cls (J) (u)$
34	3	clsss3	$⊢ (J \in Top \land u \subseteq ⋃ J) \to cls (J) (u) \subseteq ⋃ J$
35	25 31 34	syl2anc	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to cls (J) (u) \subseteq ⋃ J$
36	3	ssnei2	$⊢ ((J \in Top \land u \in nei (J) (\{y\})) \land (u \subseteq cls (J) (u) \land cls (J) (u) \subseteq ⋃ J)) \to cls (J) (u) \in nei (J) (\{y\})$
37	25 29 33 35 36	syl22anc	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to cls (J) (u) \in nei (J) (\{y\})$
38		simprrr	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to cls (J) (u) \subseteq x$
39		vex	$⊢ x \in V$
40	39	elpw2	$⊢ cls (J) (u) \in 𝒫 x \leftrightarrow cls (J) (u) \subseteq x$
41	38 40	sylibr	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to cls (J) (u) \in 𝒫 x$
42	37 41	elind	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to cls (J) (u) \in (nei (J) (\{y\}) \cap 𝒫 x)$
43	7	adantr	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to J \in Comp$
44	3	clscld	$⊢ (J \in Top \land u \subseteq ⋃ J) \to cls (J) (u) \in Clsd (J)$
45	25 31 44	syl2anc	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to cls (J) (u) \in Clsd (J)$
46		cmpcld	$⊢ (J \in Comp \land cls (J) (u) \in Clsd (J)) \to J ↾_{𝑡} cls (J) (u) \in Comp$
47	43 45 46	syl2anc	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to J ↾_{𝑡} cls (J) (u) \in Comp$
48		oveq2	$⊢ v = cls (J) (u) \to J ↾_{𝑡} v = J ↾_{𝑡} cls (J) (u)$
49	48	eleq1d	$⊢ v = cls (J) (u) \to (J ↾_{𝑡} v \in Comp \leftrightarrow J ↾_{𝑡} cls (J) (u) \in Comp)$
50	49	rspcev	$⊢ (cls (J) (u) \in (nei (J) (\{y\}) \cap 𝒫 x) \land J ↾_{𝑡} cls (J) (u) \in Comp) \to \exists v \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} v \in Comp$
51	42 47 50	syl2anc	$⊢ (((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \land (u \in J \land (y \in u \land cls (J) (u) \subseteq x))) \to \exists v \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} v \in Comp$
52	24 51	rexlimddv	$⊢ ((J \in Haus \land J \in Comp) \land (x \in J \land y \in x)) \to \exists v \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} v \in Comp$
53	52	ralrimivva	$⊢ (J \in Haus \land J \in Comp) \to \forall x \in J \forall y \in x \exists v \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} v \in Comp$
54		isnlly	$⊢ J \in N-LocallyComp\leftrightarrow(J \in Top \land \forall x \in J \forall y \in x \exists v \in (nei (J) (\{y\}) \cap 𝒫 x) J ↾_{𝑡} v \in Comp)$
55	2 53 54	sylanbrc	$⊢ (J \in Haus \land J \in Comp) \to J \in N-LocallyComp$

Metamath Proof Explorer

Theorem hausllycmp

Proof