restnlly

Description: If the property A passes to open subspaces, then a space is n-locally A iff it is locally A . (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Hypothesis	restlly.1	$⊢ (φ \land (j \in A \land x \in j)) \to j ↾_{𝑡} x \in A$
	Assertion	restnlly	$⊢ φ \to N-LocallyA=LocallyA$

Proof

Step	Hyp	Ref	Expression
1		restlly.1	$⊢ (φ \land (j \in A \land x \in j)) \to j ↾_{𝑡} x \in A$
2		nllytop	$⊢ k \in N-LocallyA\tok \in Top$
3	2	adantl	$⊢ (φ \land k \in N-LocallyA\tok \in Top)$
4		nlly2i	$⊢ (k \in N-LocallyA\landy \in k\landu \in y\to\exists s \in 𝒫 y \exists x \in k (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))$
5	4	3adant1l	$⊢ ((φ \land k \in N-LocallyA\landy \in k\landu \in y\to\exists s \in 𝒫 y \exists x \in k (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A)))$
6		simprl	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tox \in k))))$
7		simprr2	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tox \subseteq s))))$
8		simplr	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tos \in 𝒫 y))))$
9	8	elpwid	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tos \subseteq y))))$
10	7 9	sstrd	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tox \subseteq y))))$
11		velpw	$⊢ x \in 𝒫 y \leftrightarrow x \subseteq y$
12	10 11	sylibr	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tox \in 𝒫 y))))$
13	6 12	elind	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tox \in (k \cap 𝒫 y)))))$
14		simprr1	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tou \in x))))$
15		simpll1	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\to(φ \land k \in N-LocallyA)))))$
16	15 2	simpl2im	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tok \in Top))))$
17		restabs	$⊢ (k \in Top \land x \subseteq s \land s \in 𝒫 y) \to (k ↾_{𝑡} s) ↾_{𝑡} x = k ↾_{𝑡} x$
18	16 7 8 17	syl3anc	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\to(k ↾_{𝑡} s) ↾_{𝑡} x = k ↾_{𝑡} x))))$
19		df-ss	$⊢ x \subseteq s \leftrightarrow x \cap s = x$
20	7 19	sylib	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tox \cap s = x))))$
21		elrestr	$⊢ (k \in Top \land s \in 𝒫 y \land x \in k) \to x \cap s \in (k ↾_{𝑡} s)$
22	16 8 6 21	syl3anc	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tox \cap s \in (k ↾_{𝑡} s)))))$
23	20 22	eqeltrrd	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tox \in (k ↾_{𝑡} s)))))$
24		eleq2	$⊢ j = k ↾_{𝑡} s \to (x \in j \leftrightarrow x \in (k ↾_{𝑡} s))$
25		oveq1	$⊢ j = k ↾_{𝑡} s \to j ↾_{𝑡} x = (k ↾_{𝑡} s) ↾_{𝑡} x$
26	25	eleq1d	$⊢ j = k ↾_{𝑡} s \to (j ↾_{𝑡} x \in A \leftrightarrow (k ↾_{𝑡} s) ↾_{𝑡} x \in A)$
27	24 26	imbi12d	$⊢ j = k ↾_{𝑡} s \to ((x \in j \to j ↾_{𝑡} x \in A) \leftrightarrow (x \in (k ↾_{𝑡} s) \to (k ↾_{𝑡} s) ↾_{𝑡} x \in A))$
28	15	simpld	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\toφ))))$
29	1	expr	$⊢ (φ \land j \in A) \to (x \in j \to j ↾_{𝑡} x \in A)$
30	29	ralrimiva	$⊢ φ \to \forall j \in A (x \in j \to j ↾_{𝑡} x \in A)$
31	28 30	syl	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\to\forall j \in A (x \in j \to j ↾_{𝑡} x \in A)))))$
32		simprr3	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tok ↾_{𝑡} s \in A))))$
33	27 31 32	rspcdva	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\to(x \in (k ↾_{𝑡} s) \to (k ↾_{𝑡} s) ↾_{𝑡} x \in A)))))$
34	23 33	mpd	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\to(k ↾_{𝑡} s) ↾_{𝑡} x \in A))))$
35	18 34	eqeltrrd	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\tok ↾_{𝑡} x \in A))))$
36	13 14 35	jca32	$⊢ ((((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\land(x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A))\to(x \in (k \cap 𝒫 y) \land (u \in x \land k ↾_{𝑡} x \in A))))))$
37	36	ex	$⊢ (((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\to((x \in k \land (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A)) \to (x \in (k \cap 𝒫 y) \land (u \in x \land k ↾_{𝑡} x \in A))))))$
38	37	reximdv2	$⊢ (((φ \land k \in N-LocallyA\landy \in k\landu \in y\lands \in 𝒫 y\to(\exists x \in k (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A) \to \exists x \in (k \cap 𝒫 y) (u \in x \land k ↾_{𝑡} x \in A)))))$
39	38	rexlimdva	$⊢ ((φ \land k \in N-LocallyA\landy \in k\landu \in y\to(\exists s \in 𝒫 y \exists x \in k (u \in x \land x \subseteq s \land k ↾_{𝑡} s \in A) \to \exists x \in (k \cap 𝒫 y) (u \in x \land k ↾_{𝑡} x \in A))))$
40	5 39	mpd	$⊢ ((φ \land k \in N-LocallyA\landy \in k\landu \in y\to\exists x \in (k \cap 𝒫 y) (u \in x \land k ↾_{𝑡} x \in A)))$
41	40	3expb	$⊢ ((φ \land k \in N-LocallyA\land(y \in k \land u \in y)\to\exists x \in (k \cap 𝒫 y) (u \in x \land k ↾_{𝑡} x \in A)))$
42	41	ralrimivva	$⊢ (φ \land k \in N-LocallyA\to\forall y \in k \forall u \in y \exists x \in (k \cap 𝒫 y) (u \in x \land k ↾_{𝑡} x \in A))$
43		islly	$⊢ k \in LocallyA\leftrightarrow(k \in Top \land \forall y \in k \forall u \in y \exists x \in (k \cap 𝒫 y) (u \in x \land k ↾_{𝑡} x \in A))$
44	3 42 43	sylanbrc	$⊢ (φ \land k \in N-LocallyA\tok \in LocallyA)$
45	44	ex	$⊢ φ \to (k \in N-LocallyA\tok \in LocallyA)$
46	45	ssrdv	$⊢ φ \to N-LocallyA\subseteqLocallyA$
47		llyssnlly	$⊢ LocallyA\subseteqN-LocallyA$
48	47	a1i	$⊢ φ \to LocallyA\subseteqN-LocallyA$
49	46 48	eqssd	$⊢ φ \to N-LocallyA=LocallyA$

Metamath Proof Explorer

Theorem restnlly

Proof