cldllycmp

Description: A closed subspace of a locally compact space is also locally compact. (The analogous result for open subspaces follows from the more general nllyrest .) (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	cldllycmp	$⊢ (J \in N-LocallyComp\landA \in Clsd (J)\toJ ↾_{𝑡} A \in N-LocallyComp)$

Proof

Step	Hyp	Ref	Expression
1		nllytop	$⊢ J \in N-LocallyComp\toJ \in Top$
2		resttop	$⊢ (J \in Top \land A \in Clsd (J)) \to J ↾_{𝑡} A \in Top$
3	1 2	sylan	$⊢ (J \in N-LocallyComp\landA \in Clsd (J)\toJ ↾_{𝑡} A \in Top)$
4		elrest	$⊢ (J \in N-LocallyComp\landA \in Clsd (J)\to(x \in (J ↾_{𝑡} A) \leftrightarrow \exists u \in J x = u \cap A))$
5		simpll	$⊢ ((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\toJ \in N-LocallyComp))$
6		simprl	$⊢ ((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\tou \in J))$
7		simprr	$⊢ ((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\toy \in (u \cap A)))$
8	7	elin1d	$⊢ ((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\toy \in u))$
9		nlly2i	$⊢ (J \in N-LocallyComp\landu \in J\landy \in u\to\exists s \in 𝒫 u \exists w \in J (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))$
10	5 6 8 9	syl3anc	$⊢ ((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\to\exists s \in 𝒫 u \exists w \in J (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp)))$
11	3	ad2antrr	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\toJ ↾_{𝑡} A \in Top)))$
12	1	ad3antrrr	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\toJ \in Top)))$
13		simpllr	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\toA \in Clsd (J))))$
14		simprlr	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tow \in J)))$
15		elrestr	$⊢ (J \in Top \land A \in Clsd (J) \land w \in J) \to w \cap A \in (J ↾_{𝑡} A)$
16	12 13 14 15	syl3anc	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tow \cap A \in (J ↾_{𝑡} A))))$
17		simprr1	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\toy \in w)))$
18		simplrr	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\toy \in (u \cap A))))$
19	18	elin2d	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\toy \in A)))$
20	17 19	elind	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\toy \in (w \cap A))))$
21		opnneip	$⊢ (J ↾_{𝑡} A \in Top \land w \cap A \in (J ↾_{𝑡} A) \land y \in (w \cap A)) \to w \cap A \in nei (J ↾_{𝑡} A) (\{y\})$
22	11 16 20 21	syl3anc	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tow \cap A \in nei (J ↾_{𝑡} A) (\{y\}))))$
23		simprr2	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tow \subseteq s)))$
24	23	ssrind	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tow \cap A \subseteq s \cap A)))$
25		inss2	$⊢ s \cap A \subseteq A$
26		eqid	$⊢ ⋃ J = ⋃ J$
27	26	cldss	$⊢ A \in Clsd (J) \to A \subseteq ⋃ J$
28	13 27	syl	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\toA \subseteq ⋃ J)))$
29	26	restuni	$⊢ (J \in Top \land A \subseteq ⋃ J) \to A = ⋃ (J ↾_{𝑡} A)$
30	12 28 29	syl2anc	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\toA = ⋃ (J ↾_{𝑡} A))))$
31	25 30	sseqtrid	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tos \cap A \subseteq ⋃ (J ↾_{𝑡} A))))$
32		eqid	$⊢ ⋃ (J ↾_{𝑡} A) = ⋃ (J ↾_{𝑡} A)$
33	32	ssnei2	$⊢ ((J ↾_{𝑡} A \in Top \land w \cap A \in nei (J ↾_{𝑡} A) (\{y\})) \land (w \cap A \subseteq s \cap A \land s \cap A \subseteq ⋃ (J ↾_{𝑡} A))) \to s \cap A \in nei (J ↾_{𝑡} A) (\{y\})$
34	11 22 24 31 33	syl22anc	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tos \cap A \in nei (J ↾_{𝑡} A) (\{y\}))))$
35		simprll	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tos \in 𝒫 u)))$
36	35	elpwid	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tos \subseteq u)))$
37	36	ssrind	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tos \cap A \subseteq u \cap A)))$
38		vex	$⊢ s \in V$
39	38	inex1	$⊢ s \cap A \in V$
40	39	elpw	$⊢ s \cap A \in 𝒫 (u \cap A) \leftrightarrow s \cap A \subseteq u \cap A$
41	37 40	sylibr	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tos \cap A \in 𝒫 (u \cap A))))$
42	34 41	elind	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tos \cap A \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 (u \cap A)))))$
43	25	a1i	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tos \cap A \subseteq A)))$
44		restabs	$⊢ (J \in Top \land s \cap A \subseteq A \land A \in Clsd (J)) \to (J ↾_{𝑡} A) ↾_{𝑡} (s \cap A) = J ↾_{𝑡} (s \cap A)$
45	12 43 13 44	syl3anc	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\to(J ↾_{𝑡} A) ↾_{𝑡} (s \cap A) = J ↾_{𝑡} (s \cap A))))$
46		inss1	$⊢ s \cap A \subseteq s$
47	46	a1i	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tos \cap A \subseteq s)))$
48		restabs	$⊢ (J \in Top \land s \cap A \subseteq s \land s \in 𝒫 u) \to (J ↾_{𝑡} s) ↾_{𝑡} (s \cap A) = J ↾_{𝑡} (s \cap A)$
49	12 47 35 48	syl3anc	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\to(J ↾_{𝑡} s) ↾_{𝑡} (s \cap A) = J ↾_{𝑡} (s \cap A))))$
50	45 49	eqtr4d	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\to(J ↾_{𝑡} A) ↾_{𝑡} (s \cap A) = (J ↾_{𝑡} s) ↾_{𝑡} (s \cap A))))$
51		simprr3	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\toJ ↾_{𝑡} s \in Comp)))$
52		incom	$⊢ s \cap A = A \cap s$
53		eqid	$⊢ A \cap s = A \cap s$
54		ineq1	$⊢ v = A \to v \cap s = A \cap s$
55	54	rspceeqv	$⊢ (A \in Clsd (J) \land A \cap s = A \cap s) \to \exists v \in Clsd (J) A \cap s = v \cap s$
56	13 53 55	sylancl	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\to\exists v \in Clsd (J) A \cap s = v \cap s)))$
57		simplrl	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tou \in J)))$
58		elssuni	$⊢ u \in J \to u \subseteq ⋃ J$
59	57 58	syl	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tou \subseteq ⋃ J)))$
60	36 59	sstrd	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tos \subseteq ⋃ J)))$
61	26	restcld	$⊢ (J \in Top \land s \subseteq ⋃ J) \to (A \cap s \in Clsd (J ↾_{𝑡} s) \leftrightarrow \exists v \in Clsd (J) A \cap s = v \cap s)$
62	12 60 61	syl2anc	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\to(A \cap s \in Clsd (J ↾_{𝑡} s) \leftrightarrow \exists v \in Clsd (J) A \cap s = v \cap s))))$
63	56 62	mpbird	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\toA \cap s \in Clsd (J ↾_{𝑡} s))))$
64	52 63	eqeltrid	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\tos \cap A \in Clsd (J ↾_{𝑡} s))))$
65		cmpcld	$⊢ (J ↾_{𝑡} s \in Comp \land s \cap A \in Clsd (J ↾_{𝑡} s)) \to (J ↾_{𝑡} s) ↾_{𝑡} (s \cap A) \in Comp$
66	51 64 65	syl2anc	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\to(J ↾_{𝑡} s) ↾_{𝑡} (s \cap A) \in Comp)))$
67	50 66	eqeltrd	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\to(J ↾_{𝑡} A) ↾_{𝑡} (s \cap A) \in Comp)))$
68		oveq2	$⊢ v = s \cap A \to (J ↾_{𝑡} A) ↾_{𝑡} v = (J ↾_{𝑡} A) ↾_{𝑡} (s \cap A)$
69	68	eleq1d	$⊢ v = s \cap A \to ((J ↾_{𝑡} A) ↾_{𝑡} v \in Comp \leftrightarrow (J ↾_{𝑡} A) ↾_{𝑡} (s \cap A) \in Comp)$
70	69	rspcev	$⊢ (s \cap A \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 (u \cap A)) \land (J ↾_{𝑡} A) ↾_{𝑡} (s \cap A) \in Comp) \to \exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 (u \cap A)) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp$
71	42 67 70	syl2anc	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land((s \in 𝒫 u \land w \in J) \land (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp))\to\exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 (u \cap A)) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp)))$
72	71	expr	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\land(s \in 𝒫 u \land w \in J)\to((y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp) \to \exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 (u \cap A)) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp))))$
73	72	rexlimdvva	$⊢ ((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\to(\exists s \in 𝒫 u \exists w \in J (y \in w \land w \subseteq s \land J ↾_{𝑡} s \in Comp) \to \exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 (u \cap A)) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp)))$
74	10 73	mpd	$⊢ ((J \in N-LocallyComp\landA \in Clsd (J)\land(u \in J \land y \in (u \cap A))\to\exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 (u \cap A)) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp))$
75	74	anassrs	$⊢ (((J \in N-LocallyComp\landA \in Clsd (J)\landu \in J\landy \in (u \cap A)\to\exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 (u \cap A)) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp)))$
76	75	ralrimiva	$⊢ ((J \in N-LocallyComp\landA \in Clsd (J)\landu \in J\to\forall y \in (u \cap A) \exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 (u \cap A)) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp))$
77		pweq	$⊢ x = u \cap A \to 𝒫 x = 𝒫 (u \cap A)$
78	77	ineq2d	$⊢ x = u \cap A \to nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 x = nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 (u \cap A)$
79	78	rexeqdv	$⊢ x = u \cap A \to (\exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp \leftrightarrow \exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 (u \cap A)) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp)$
80	79	raleqbi1dv	$⊢ x = u \cap A \to (\forall y \in x \exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp \leftrightarrow \forall y \in (u \cap A) \exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 (u \cap A)) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp)$
81	76 80	syl5ibrcom	$⊢ ((J \in N-LocallyComp\landA \in Clsd (J)\landu \in J\to(x = u \cap A \to \forall y \in x \exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp)))$
82	81	rexlimdva	$⊢ (J \in N-LocallyComp\landA \in Clsd (J)\to(\exists u \in J x = u \cap A \to \forall y \in x \exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp))$
83	4 82	sylbid	$⊢ (J \in N-LocallyComp\landA \in Clsd (J)\to(x \in (J ↾_{𝑡} A) \to \forall y \in x \exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp))$
84	83	ralrimiv	$⊢ (J \in N-LocallyComp\landA \in Clsd (J)\to\forall x \in (J ↾_{𝑡} A) \forall y \in x \exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp)$
85		isnlly	$⊢ J ↾_{𝑡} A \in N-LocallyComp\leftrightarrow(J ↾_{𝑡} A \in Top \land \forall x \in (J ↾_{𝑡} A) \forall y \in x \exists v \in (nei (J ↾_{𝑡} A) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} A) ↾_{𝑡} v \in Comp)$
86	3 84 85	sylanbrc	$⊢ (J \in N-LocallyComp\landA \in Clsd (J)\toJ ↾_{𝑡} A \in N-LocallyComp)$

Metamath Proof Explorer

Theorem cldllycmp

Proof