nllyrest

Description: An open subspace of an n-locally A space is also n-locally A . (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	nllyrest	$⊢ (J \in N-LocallyA\landB \in J\toJ ↾_{𝑡} B \in N-LocallyA)$

Proof

Step	Hyp	Ref	Expression
1		nllytop	$⊢ J \in N-LocallyA\toJ \in Top$
2		resttop	$⊢ (J \in Top \land B \in J) \to J ↾_{𝑡} B \in Top$
3	1 2	sylan	$⊢ (J \in N-LocallyA\landB \in J\toJ ↾_{𝑡} B \in Top)$
4		restopn2	$⊢ (J \in Top \land B \in J) \to (x \in (J ↾_{𝑡} B) \leftrightarrow (x \in J \land x \subseteq B))$
5	1 4	sylan	$⊢ (J \in N-LocallyA\landB \in J\to(x \in (J ↾_{𝑡} B) \leftrightarrow (x \in J \land x \subseteq B)))$
6		simp1l	$⊢ ((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\toJ \in N-LocallyA))$
7		simp2l	$⊢ ((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\tox \in J))$
8		simp3	$⊢ ((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\toy \in x))$
9		nlly2i	$⊢ (J \in N-LocallyA\landx \in J\landy \in x\to\exists s \in 𝒫 x \exists u \in J (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))$
10	6 7 8 9	syl3anc	$⊢ ((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\to\exists s \in 𝒫 x \exists u \in J (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A)))$
11	3	3ad2ant1	$⊢ ((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\toJ ↾_{𝑡} B \in Top))$
12	11	3ad2ant1	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\toJ ↾_{𝑡} B \in Top)))$
13		simp3l	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\tou \in J)))$
14		simp3r2	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\tou \subseteq s)))$
15		simp2	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\tos \in 𝒫 x)))$
16	15	elpwid	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\tos \subseteq x)))$
17		simp12r	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\tox \subseteq B)))$
18	16 17	sstrd	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\tos \subseteq B)))$
19	14 18	sstrd	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\tou \subseteq B)))$
20	6	3ad2ant1	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\toJ \in N-LocallyA)))$
21	20 1	syl	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\toJ \in Top)))$
22		simp11r	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\toB \in J)))$
23		restopn2	$⊢ (J \in Top \land B \in J) \to (u \in (J ↾_{𝑡} B) \leftrightarrow (u \in J \land u \subseteq B))$
24	21 22 23	syl2anc	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\to(u \in (J ↾_{𝑡} B) \leftrightarrow (u \in J \land u \subseteq B)))))$
25	13 19 24	mpbir2and	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\tou \in (J ↾_{𝑡} B))))$
26		simp3r1	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\toy \in u)))$
27		opnneip	$⊢ (J ↾_{𝑡} B \in Top \land u \in (J ↾_{𝑡} B) \land y \in u) \to u \in nei (J ↾_{𝑡} B) (\{y\})$
28	12 25 26 27	syl3anc	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\tou \in nei (J ↾_{𝑡} B) (\{y\}))))$
29		elssuni	$⊢ B \in J \to B \subseteq ⋃ J$
30	22 29	syl	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\toB \subseteq ⋃ J)))$
31		eqid	$⊢ ⋃ J = ⋃ J$
32	31	restuni	$⊢ (J \in Top \land B \subseteq ⋃ J) \to B = ⋃ (J ↾_{𝑡} B)$
33	21 30 32	syl2anc	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\toB = ⋃ (J ↾_{𝑡} B))))$
34	18 33	sseqtrd	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\tos \subseteq ⋃ (J ↾_{𝑡} B))))$
35		eqid	$⊢ ⋃ (J ↾_{𝑡} B) = ⋃ (J ↾_{𝑡} B)$
36	35	ssnei2	$⊢ ((J ↾_{𝑡} B \in Top \land u \in nei (J ↾_{𝑡} B) (\{y\})) \land (u \subseteq s \land s \subseteq ⋃ (J ↾_{𝑡} B))) \to s \in nei (J ↾_{𝑡} B) (\{y\})$
37	12 28 14 34 36	syl22anc	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\tos \in nei (J ↾_{𝑡} B) (\{y\}))))$
38	37 15	elind	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\tos \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x))))$
39		restabs	$⊢ (J \in Top \land s \subseteq B \land B \in J) \to (J ↾_{𝑡} B) ↾_{𝑡} s = J ↾_{𝑡} s$
40	21 18 22 39	syl3anc	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\to(J ↾_{𝑡} B) ↾_{𝑡} s = J ↾_{𝑡} s)))$
41		simp3r3	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\toJ ↾_{𝑡} s \in A)))$
42	40 41	eqeltrd	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\to(J ↾_{𝑡} B) ↾_{𝑡} s \in A)))$
43	38 42	jca	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\to(s \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x) \land (J ↾_{𝑡} B) ↾_{𝑡} s \in A))))$
44	43	3expa	$⊢ ((((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\land(u \in J \land (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A))\to(s \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x) \land (J ↾_{𝑡} B) ↾_{𝑡} s \in A)))))$
45	44	rexlimdvaa	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\lands \in 𝒫 x\to(\exists u \in J (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A) \to (s \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x) \land (J ↾_{𝑡} B) ↾_{𝑡} s \in A)))))$
46	45	expimpd	$⊢ ((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\to((s \in 𝒫 x \land \exists u \in J (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A)) \to (s \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x) \land (J ↾_{𝑡} B) ↾_{𝑡} s \in A))))$
47	46	reximdv2	$⊢ ((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\to(\exists s \in 𝒫 x \exists u \in J (y \in u \land u \subseteq s \land J ↾_{𝑡} s \in A) \to \exists s \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} B) ↾_{𝑡} s \in A)))$
48	10 47	mpd	$⊢ ((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\to\exists s \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} B) ↾_{𝑡} s \in A))$
49	48	3expa	$⊢ (((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\to\exists s \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} B) ↾_{𝑡} s \in A)))$
50	49	ralrimiva	$⊢ ((J \in N-LocallyA\landB \in J\land(x \in J \land x \subseteq B)\to\forall y \in x \exists s \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} B) ↾_{𝑡} s \in A))$
51	50	ex	$⊢ (J \in N-LocallyA\landB \in J\to((x \in J \land x \subseteq B) \to \forall y \in x \exists s \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} B) ↾_{𝑡} s \in A))$
52	5 51	sylbid	$⊢ (J \in N-LocallyA\landB \in J\to(x \in (J ↾_{𝑡} B) \to \forall y \in x \exists s \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} B) ↾_{𝑡} s \in A))$
53	52	ralrimiv	$⊢ (J \in N-LocallyA\landB \in J\to\forall x \in (J ↾_{𝑡} B) \forall y \in x \exists s \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} B) ↾_{𝑡} s \in A)$
54		isnlly	$⊢ J ↾_{𝑡} B \in N-LocallyA\leftrightarrow(J ↾_{𝑡} B \in Top \land \forall x \in (J ↾_{𝑡} B) \forall y \in x \exists s \in (nei (J ↾_{𝑡} B) (\{y\}) \cap 𝒫 x) (J ↾_{𝑡} B) ↾_{𝑡} s \in A)$
55	3 53 54	sylanbrc	$⊢ (J \in N-LocallyA\landB \in J\toJ ↾_{𝑡} B \in N-LocallyA)$

Metamath Proof Explorer

Theorem nllyrest

Proof