llyrest

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

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

Proof

Step	Hyp	Ref	Expression
1		llytop	$⊢ J \in LocallyA\toJ \in Top$
2		resttop	$⊢ (J \in Top \land B \in J) \to J ↾_{𝑡} B \in Top$
3	1 2	sylan	$⊢ (J \in 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 LocallyA\landB \in J\to(x \in (J ↾_{𝑡} B) \leftrightarrow (x \in J \land x \subseteq B)))$
6		simp1l	$⊢ ((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\toJ \in LocallyA))$
7		simp2l	$⊢ ((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\tox \in J))$
8		simp3	$⊢ ((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\toy \in x))$
9		llyi	$⊢ (J \in LocallyA\landx \in J\landy \in x\to\exists v \in J (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))$
10	6 7 8 9	syl3anc	$⊢ ((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\to\exists v \in J (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A)))$
11		simprl	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\tov \in J)))$
12		simprr1	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\tov \subseteq x)))$
13		simpl2r	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\tox \subseteq B)))$
14	12 13	sstrd	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\tov \subseteq B)))$
15	6 1	syl	$⊢ ((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\toJ \in Top))$
16	15	adantr	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\toJ \in Top)))$
17		simpl1r	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\toB \in J)))$
18		restopn2	$⊢ (J \in Top \land B \in J) \to (v \in (J ↾_{𝑡} B) \leftrightarrow (v \in J \land v \subseteq B))$
19	16 17 18	syl2anc	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\to(v \in (J ↾_{𝑡} B) \leftrightarrow (v \in J \land v \subseteq B)))))$
20	11 14 19	mpbir2and	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\tov \in (J ↾_{𝑡} B))))$
21		velpw	$⊢ v \in 𝒫 x \leftrightarrow v \subseteq x$
22	12 21	sylibr	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\tov \in 𝒫 x)))$
23	20 22	elind	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\tov \in ((J ↾_{𝑡} B) \cap 𝒫 x))))$
24		simprr2	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\toy \in v)))$
25		restabs	$⊢ (J \in Top \land v \subseteq B \land B \in J) \to (J ↾_{𝑡} B) ↾_{𝑡} v = J ↾_{𝑡} v$
26	16 14 17 25	syl3anc	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\to(J ↾_{𝑡} B) ↾_{𝑡} v = J ↾_{𝑡} v)))$
27		simprr3	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\toJ ↾_{𝑡} v \in A)))$
28	26 27	eqeltrd	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\to(J ↾_{𝑡} B) ↾_{𝑡} v \in A)))$
29	23 24 28	jca32	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\land(v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A))\to(v \in ((J ↾_{𝑡} B) \cap 𝒫 x) \land (y \in v \land (J ↾_{𝑡} B) ↾_{𝑡} v \in A)))))$
30	29	ex	$⊢ ((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\to((v \in J \land (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A)) \to (v \in ((J ↾_{𝑡} B) \cap 𝒫 x) \land (y \in v \land (J ↾_{𝑡} B) ↾_{𝑡} v \in A)))))$
31	30	reximdv2	$⊢ ((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\to(\exists v \in J (v \subseteq x \land y \in v \land J ↾_{𝑡} v \in A) \to \exists v \in ((J ↾_{𝑡} B) \cap 𝒫 x) (y \in v \land (J ↾_{𝑡} B) ↾_{𝑡} v \in A))))$
32	10 31	mpd	$⊢ ((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\to\exists v \in ((J ↾_{𝑡} B) \cap 𝒫 x) (y \in v \land (J ↾_{𝑡} B) ↾_{𝑡} v \in A)))$
33	32	3expa	$⊢ (((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\landy \in x\to\exists v \in ((J ↾_{𝑡} B) \cap 𝒫 x) (y \in v \land (J ↾_{𝑡} B) ↾_{𝑡} v \in A))))$
34	33	ralrimiva	$⊢ ((J \in LocallyA\landB \in J\land(x \in J \land x \subseteq B)\to\forall y \in x \exists v \in ((J ↾_{𝑡} B) \cap 𝒫 x) (y \in v \land (J ↾_{𝑡} B) ↾_{𝑡} v \in A)))$
35	34	ex	$⊢ (J \in LocallyA\landB \in J\to((x \in J \land x \subseteq B) \to \forall y \in x \exists v \in ((J ↾_{𝑡} B) \cap 𝒫 x) (y \in v \land (J ↾_{𝑡} B) ↾_{𝑡} v \in A)))$
36	5 35	sylbid	$⊢ (J \in LocallyA\landB \in J\to(x \in (J ↾_{𝑡} B) \to \forall y \in x \exists v \in ((J ↾_{𝑡} B) \cap 𝒫 x) (y \in v \land (J ↾_{𝑡} B) ↾_{𝑡} v \in A)))$
37	36	ralrimiv	$⊢ (J \in LocallyA\landB \in J\to\forall x \in (J ↾_{𝑡} B) \forall y \in x \exists v \in ((J ↾_{𝑡} B) \cap 𝒫 x) (y \in v \land (J ↾_{𝑡} B) ↾_{𝑡} v \in A))$
38		islly	$⊢ J ↾_{𝑡} B \in LocallyA\leftrightarrow(J ↾_{𝑡} B \in Top \land \forall x \in (J ↾_{𝑡} B) \forall y \in x \exists v \in ((J ↾_{𝑡} B) \cap 𝒫 x) (y \in v \land (J ↾_{𝑡} B) ↾_{𝑡} v \in A))$
39	3 37 38	sylanbrc	$⊢ (J \in LocallyA\landB \in J\toJ ↾_{𝑡} B \in LocallyA)$

Metamath Proof Explorer

Theorem llyrest

Proof