llyidm

Description: Idempotence of the "locally" predicate, i.e. being "locally A " is a local property. (Contributed by Mario Carneiro, 2-Mar-2015)

		Ref	Expression
	Assertion	llyidm	$⊢ LocallyLocallyA=LocallyA$

Proof

Step	Hyp	Ref	Expression
1		llytop	$⊢ j \in LocallyLocallyA\toj \in Top$
2		llyi	$⊢ (j \in LocallyLocallyA\landx \in j\landy \in x\to\exists u \in j (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))$
3		simprr3	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\toj ↾_{𝑡} u \in LocallyA))$
4		simprl	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\tou \in j))$
5		ssidd	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\tou \subseteq u))$
6	1	3ad2ant1	$⊢ (j \in LocallyLocallyA\landx \in j\landy \in x\toj \in Top)$
7	6	adantr	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in 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 LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\to(u \in (j ↾_{𝑡} u) \leftrightarrow (u \in j \land u \subseteq u))))$
10	4 5 9	mpbir2and	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\tou \in (j ↾_{𝑡} u)))$
11		simprr2	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\toy \in u))$
12		llyi	$⊢ (j ↾_{𝑡} u \in LocallyA\landu \in (j ↾_{𝑡} u)\landy \in u\to\exists v \in (j ↾_{𝑡} u) (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))$
13	3 10 11 12	syl3anc	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\to\exists v \in (j ↾_{𝑡} u) (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A)))$
14		restopn2	$⊢ (j \in Top \land u \in j) \to (v \in (j ↾_{𝑡} u) \leftrightarrow (v \in j \land v \subseteq u))$
15	7 4 14	syl2anc	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\to(v \in (j ↾_{𝑡} u) \leftrightarrow (v \in j \land v \subseteq u))))$
16		simpl	$⊢ (v \in j \land v \subseteq u) \to v \in j$
17	15 16	biimtrdi	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\to(v \in (j ↾_{𝑡} u) \to v \in j)))$
18		simprl	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tov \in j)))$
19		simprr1	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tov \subseteq u)))$
20		simprr1	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\tou \subseteq x))$
21	20	adantr	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tou \subseteq x)))$
22	19 21	sstrd	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tov \subseteq x)))$
23		velpw	$⊢ v \in 𝒫 x \leftrightarrow v \subseteq x$
24	22 23	sylibr	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tov \in 𝒫 x)))$
25	18 24	elind	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tov \in (j \cap 𝒫 x))))$
26		simprr2	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\toy \in v)))$
27	7	adantr	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\toj \in Top)))$
28		simplrl	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\tou \in j)))$
29		restabs	$⊢ (j \in Top \land v \subseteq u \land u \in j) \to (j ↾_{𝑡} u) ↾_{𝑡} v = j ↾_{𝑡} v$
30	27 19 28 29	syl3anc	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\to(j ↾_{𝑡} u) ↾_{𝑡} v = j ↾_{𝑡} v)))$
31		simprr3	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\to(j ↾_{𝑡} u) ↾_{𝑡} v \in A)))$
32	30 31	eqeltrrd	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\toj ↾_{𝑡} v \in A)))$
33	25 26 32	jca32	$⊢ (((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\land(v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A))\to(v \in (j \cap 𝒫 x) \land (y \in v \land j ↾_{𝑡} v \in A)))))$
34	33	ex	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\to((v \in j \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A)) \to (v \in (j \cap 𝒫 x) \land (y \in v \land j ↾_{𝑡} v \in A)))))$
35	17 34	syland	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\to((v \in (j ↾_{𝑡} u) \land (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A)) \to (v \in (j \cap 𝒫 x) \land (y \in v \land j ↾_{𝑡} v \in A)))))$
36	35	reximdv2	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\to(\exists v \in (j ↾_{𝑡} u) (v \subseteq u \land y \in v \land (j ↾_{𝑡} u) ↾_{𝑡} v \in A) \to \exists v \in (j \cap 𝒫 x) (y \in v \land j ↾_{𝑡} v \in A))))$
37	13 36	mpd	$⊢ ((j \in LocallyLocallyA\landx \in j\landy \in x\land(u \in j \land (u \subseteq x \land y \in u \land j ↾_{𝑡} u \in LocallyA))\to\exists v \in (j \cap 𝒫 x) (y \in v \land j ↾_{𝑡} v \in A)))$
38	2 37	rexlimddv	$⊢ (j \in LocallyLocallyA\landx \in j\landy \in x\to\exists v \in (j \cap 𝒫 x) (y \in v \land j ↾_{𝑡} v \in A))$
39	38	3expb	$⊢ (j \in LocallyLocallyA\land(x \in j \land y \in x)\to\exists v \in (j \cap 𝒫 x) (y \in v \land j ↾_{𝑡} v \in A))$
40	39	ralrimivva	$⊢ j \in LocallyLocallyA\to\forall x \in j \forall y \in x \exists v \in (j \cap 𝒫 x) (y \in v \land j ↾_{𝑡} v \in A)$
41		islly	$⊢ j \in LocallyA\leftrightarrow(j \in Top \land \forall x \in j \forall y \in x \exists v \in (j \cap 𝒫 x) (y \in v \land j ↾_{𝑡} v \in A))$
42	1 40 41	sylanbrc	$⊢ j \in LocallyLocallyA\toj \in LocallyA$
43	42	ssriv	$⊢ LocallyLocallyA\subseteqLocallyA$
44		llyrest	$⊢ (j \in LocallyA\landx \in j\toj ↾_{𝑡} x \in LocallyA)$
45	44	adantl	$⊢ (⊤ \land (j \in LocallyA\landx \in j\toj ↾_{𝑡} x \in LocallyA))$
46		llytop	$⊢ j \in LocallyA\toj \in Top$
47	46	ssriv	$⊢ LocallyA\subseteqTop$
48	47	a1i	$⊢ ⊤ \to LocallyA\subseteqTop$
49	45 48	restlly	$⊢ ⊤ \to LocallyA\subseteqLocallyLocallyA$
50	49	mptru	$⊢ LocallyA\subseteqLocallyLocallyA$
51	43 50	eqssi	$⊢ LocallyLocallyA=LocallyA$

Metamath Proof Explorer

Theorem llyidm

Proof