nllyidm

Description: Idempotence of the "n-locally" predicate, i.e. being "n-locally A " is a local property. (Use loclly to show N-Locally N-Locally A = N-Locally A .) (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	nllyidm	$⊢ LocallyN-LocallyA=N-LocallyA$

Proof

Step	Hyp	Ref	Expression
1		llytop	$⊢ j \in LocallyN-LocallyA\toj \in Top$
2		llyi	$⊢ (j \in LocallyN-LocallyA\landx \in j\landy \in x\to\exists u \in j)$
3		simprr3	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\toj ↾_{𝑡} u \in N-LocallyA))$
4		simprl	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\tou \in j))$
5		ssidd	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\tou \subseteq u))$
6		simpl1	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\toj \in LocallyN-LocallyA))$
7	6 1	syl	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\toj \in Top))$
8		restopn2	$⊢ (j \in Top \land u \in j) \to (u \in (j ↾_{𝑡} u) \leftrightarrow (u \in j \land u \subseteq u))$
9	7 4 8	syl2anc	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\to(u \in (j ↾_{𝑡} u) \leftrightarrow (u \in j \land u \subseteq u))))$
10	4 5 9	mpbir2and	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\tou \in (j ↾_{𝑡} u)))$
11		simprr2	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\toy \in u))$
12		nlly2i	$⊢ (j ↾_{𝑡} u \in N-LocallyA\landu \in (j ↾_{𝑡} u)\landy \in u\to\exists v \in 𝒫 u)$
13	3 10 11 12	syl3anc	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\to\exists v \in 𝒫 u))$
14		restopn2	$⊢ (j \in Top \land u \in j) \to (z \in (j ↾_{𝑡} u) \leftrightarrow (z \in j \land z \subseteq u))$
15	7 4 14	syl2anc	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\to(z \in (j ↾_{𝑡} u) \leftrightarrow (z \in j \land z \subseteq u))))$
16	15	adantr	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\landv \in 𝒫 u\to(z \in (j ↾_{𝑡} u) \leftrightarrow (z \in j \land z \subseteq u)))))$
17	7	adantr	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\toj \in Top)))$
18		simpr2l	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\toz \in j)))$
19		simpr31	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\toy \in z)))$
20		opnneip	$⊢ (j \in Top \land z \in j \land y \in z) \to z \in nei (j) (\{y\})$
21	17 18 19 20	syl3anc	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\toz \in nei (j) (\{y\}))))$
22		simpr32	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\toz \subseteq v)))$
23		simpr1	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tov \in 𝒫 u)))$
24	23	elpwid	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tov \subseteq u)))$
25	4	adantr	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tou \in j)))$
26		elssuni	$⊢ u \in j \to u \subseteq ⋃ j$
27	25 26	syl	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tou \subseteq ⋃ j)))$
28	24 27	sstrd	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tov \subseteq ⋃ j)))$
29		eqid	$⊢ ⋃ j = ⋃ j$
30	29	ssnei2	$⊢ ((j \in Top \land z \in nei (j) (\{y\})) \land (z \subseteq v \land v \subseteq ⋃ j)) \to v \in nei (j) (\{y\})$
31	17 21 22 28 30	syl22anc	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tov \in nei (j) (\{y\}))))$
32		simprr1	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\tou \subseteq x))$
33	32	adantr	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tou \subseteq x)))$
34	24 33	sstrd	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tov \subseteq x)))$
35		velpw	$⊢ v \in 𝒫 x \leftrightarrow v \subseteq x$
36	34 35	sylibr	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tov \in 𝒫 x)))$
37	31 36	elind	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tov \in (nei (j) (\{y\}) \cap 𝒫 x))))$
38		restabs	$⊢ (j \in Top \land v \subseteq u \land u \in j) \to (j ↾_{𝑡} u) ↾_{𝑡} v = j ↾_{𝑡} v$
39	17 24 25 38	syl3anc	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\to(j ↾_{𝑡} u) ↾_{𝑡} v = j ↾_{𝑡} v)))$
40		simpr33	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\to(j ↾_{𝑡} u) ↾_{𝑡} v \in A)))$
41	39 40	eqeltrrd	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\toj ↾_{𝑡} v \in A)))$
42	37 41	jca	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\land(v \in 𝒫 u \land (z \in j \land z \subseteq u) \land (y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\to(v \in (nei (j) (\{y\}) \cap 𝒫 x) \land j ↾_{𝑡} v \in A))))$
43	42	3exp2	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\to(v \in 𝒫 u \to ((z \in j \land z \subseteq u) \to ((y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A) \to (v \in (nei (j) (\{y\}) \cap 𝒫 x) \land j ↾_{𝑡} v \in A))))))$
44	43	imp	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\landv \in 𝒫 u\to((z \in j \land z \subseteq u) \to ((y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A) \to (v \in (nei (j) (\{y\}) \cap 𝒫 x) \land j ↾_{𝑡} v \in A))))))$
45	16 44	sylbid	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\landv \in 𝒫 u\to(z \in (j ↾_{𝑡} u) \to ((y \in z \land z \subseteq v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A) \to (v \in (nei (j) (\{y\}) \cap 𝒫 x) \land j ↾_{𝑡} v \in A))))))$
46	45	rexlimdv	$⊢ (((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\landv \in 𝒫 u\to(\exists z \in (j ↾_{𝑡} u) \to (v \in (nei (j) (\{y\}) \cap 𝒫 x) \land j ↾_{𝑡} v \in A)))))$
47	46	expimpd	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\to((v \in 𝒫 u \land \exists z \in (j ↾_{𝑡} u)) \to (v \in (nei (j) (\{y\}) \cap 𝒫 x) \land j ↾_{𝑡} v \in A))))$
48	47	reximdv2	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\to(\exists v \in 𝒫 u \to \exists v \in (nei (j) (\{y\}) \cap 𝒫 x))))$
49	13 48	mpd	$⊢ ((j \in LocallyN-LocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in N-LocallyA))\to\exists v \in (nei (j) (\{y\}) \cap 𝒫 x)))$
50	2 49	rexlimddv	$⊢ (j \in LocallyN-LocallyA\landx \in j\landy \in x\to\exists v \in (nei (j) (\{y\}) \cap 𝒫 x))$
51	50	3expb	$⊢ (j \in LocallyN-LocallyA\land(x \in j \land y \in x)\to\exists v \in (nei (j) (\{y\}) \cap 𝒫 x))$
52	51	ralrimivva	$⊢ j \in LocallyN-LocallyA\to\forall x \in j$
53		isnlly	$⊢ j \in N-LocallyA\leftrightarrow(j \in Top \land \forall x \in j)$
54	1 52 53	sylanbrc	$⊢ j \in LocallyN-LocallyA\toj \in N-LocallyA$
55	54	ssriv	$⊢ LocallyN-LocallyA\subseteqN-LocallyA$
56		nllyrest	$⊢ (j \in N-LocallyA\landx \in j\toj ↾_{𝑡} x \in N-LocallyA)$
57	56	adantl	$⊢ (⊤ \land (j \in N-LocallyA\landx \in j\toj ↾_{𝑡} x \in N-LocallyA))$
58		nllytop	$⊢ j \in N-LocallyA\toj \in Top$
59	58	ssriv	$⊢ N-LocallyA\subseteqTop$
60	59	a1i	$⊢ ⊤ \to N-LocallyA\subseteqTop$
61	57 60	restlly	$⊢ ⊤ \to N-LocallyA\subseteqLocallyN-LocallyA$
62	61	mptru	$⊢ N-LocallyA\subseteqLocallyN-LocallyA$
63	55 62	eqssi	$⊢ LocallyN-LocallyA=N-LocallyA$

Metamath Proof Explorer

Theorem nllyidm

Proof