subislly

Description: The property of a subspace being locally A . (Contributed by Mario Carneiro, 10-Mar-2015)

		Ref	Expression
	Assertion	subislly	$⊢ (J \in Top \land B \in V) \to (J ↾_{𝑡} B \in LocallyA\leftrightarrow\forall x \in J \forall y \in (x \cap B) \exists u \in J (u \cap B \subseteq x \land y \in u \land J ↾_{𝑡} (u \cap B) \in A))$

Proof

Step	Hyp	Ref	Expression
1		resttop	$⊢ (J \in Top \land B \in V) \to J ↾_{𝑡} B \in Top$
2		islly	$⊢ J ↾_{𝑡} B \in LocallyA\leftrightarrow(J ↾_{𝑡} B \in Top \land \forall z \in (J ↾_{𝑡} B) \forall y \in z \exists w \in ((J ↾_{𝑡} B) \cap 𝒫 z) (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A))$
3	2	baib	$⊢ J ↾_{𝑡} B \in Top \to (J ↾_{𝑡} B \in LocallyA\leftrightarrow\forall z \in (J ↾_{𝑡} B) \forall y \in z \exists w \in ((J ↾_{𝑡} B) \cap 𝒫 z) (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A))$
4	1 3	syl	$⊢ (J \in Top \land B \in V) \to (J ↾_{𝑡} B \in LocallyA\leftrightarrow\forall z \in (J ↾_{𝑡} B) \forall y \in z \exists w \in ((J ↾_{𝑡} B) \cap 𝒫 z) (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A))$
5		vex	$⊢ x \in V$
6	5	inex1	$⊢ x \cap B \in V$
7	6	a1i	$⊢ ((J \in Top \land B \in V) \land x \in J) \to x \cap B \in V$
8		elrest	$⊢ (J \in Top \land B \in V) \to (z \in (J ↾_{𝑡} B) \leftrightarrow \exists x \in J z = x \cap B)$
9		simpr	$⊢ ((J \in Top \land B \in V) \land z = x \cap B) \to z = x \cap B$
10	9	raleqdv	$⊢ ((J \in Top \land B \in V) \land z = x \cap B) \to (\forall y \in z \exists w \in ((J ↾_{𝑡} B) \cap 𝒫 z) (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A) \leftrightarrow \forall y \in (x \cap B) \exists w \in ((J ↾_{𝑡} B) \cap 𝒫 z) (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A))$
11		rexin	$⊢ \exists w \in ((J ↾_{𝑡} B) \cap 𝒫 z) (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A) \leftrightarrow \exists w \in (J ↾_{𝑡} B) (w \in 𝒫 z \land (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A))$
12		vex	$⊢ u \in V$
13	12	inex1	$⊢ u \cap B \in V$
14	13	a1i	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land u \in J) \to u \cap B \in V$
15		elrest	$⊢ (J \in Top \land B \in V) \to (w \in (J ↾_{𝑡} B) \leftrightarrow \exists u \in J w = u \cap B)$
16	15	ad2antrr	$⊢ (((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \to (w \in (J ↾_{𝑡} B) \leftrightarrow \exists u \in J w = u \cap B)$
17		3anass	$⊢ (w \in 𝒫 z \land y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A) \leftrightarrow (w \in 𝒫 z \land (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A))$
18		simpr	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to w = u \cap B$
19		simpllr	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to z = x \cap B$
20	18 19	sseq12d	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to (w \subseteq z \leftrightarrow u \cap B \subseteq x \cap B)$
21		velpw	$⊢ w \in 𝒫 z \leftrightarrow w \subseteq z$
22		inss2	$⊢ u \cap B \subseteq B$
23	22	biantru	$⊢ u \cap B \subseteq x \leftrightarrow (u \cap B \subseteq x \land u \cap B \subseteq B)$
24		ssin	$⊢ (u \cap B \subseteq x \land u \cap B \subseteq B) \leftrightarrow u \cap B \subseteq x \cap B$
25	23 24	bitri	$⊢ u \cap B \subseteq x \leftrightarrow u \cap B \subseteq x \cap B$
26	20 21 25	3bitr4g	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to (w \in 𝒫 z \leftrightarrow u \cap B \subseteq x)$
27	18	eleq2d	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to (y \in w \leftrightarrow y \in (u \cap B))$
28		simplr	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to y \in (x \cap B)$
29	28	elin2d	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to y \in B$
30	29	biantrud	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to (y \in u \leftrightarrow (y \in u \land y \in B))$
31		elin	$⊢ y \in (u \cap B) \leftrightarrow (y \in u \land y \in B)$
32	30 31	bitr4di	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to (y \in u \leftrightarrow y \in (u \cap B))$
33	27 32	bitr4d	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to (y \in w \leftrightarrow y \in u)$
34	18	oveq2d	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to (J ↾_{𝑡} B) ↾_{𝑡} w = (J ↾_{𝑡} B) ↾_{𝑡} (u \cap B)$
35		simp-4l	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to J \in Top$
36	22	a1i	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to u \cap B \subseteq B$
37		simplr	$⊢ ((J \in Top \land B \in V) \land z = x \cap B) \to B \in V$
38	37	ad2antrr	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to B \in V$
39		restabs	$⊢ (J \in Top \land u \cap B \subseteq B \land B \in V) \to (J ↾_{𝑡} B) ↾_{𝑡} (u \cap B) = J ↾_{𝑡} (u \cap B)$
40	35 36 38 39	syl3anc	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to (J ↾_{𝑡} B) ↾_{𝑡} (u \cap B) = J ↾_{𝑡} (u \cap B)$
41	34 40	eqtrd	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to (J ↾_{𝑡} B) ↾_{𝑡} w = J ↾_{𝑡} (u \cap B)$
42	41	eleq1d	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to ((J ↾_{𝑡} B) ↾_{𝑡} w \in A \leftrightarrow J ↾_{𝑡} (u \cap B) \in A)$
43	26 33 42	3anbi123d	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to ((w \in 𝒫 z \land y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A) \leftrightarrow (u \cap B \subseteq x \land y \in u \land J ↾_{𝑡} (u \cap B) \in A))$
44	17 43	bitr3id	$⊢ ((((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \land w = u \cap B) \to ((w \in 𝒫 z \land (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A)) \leftrightarrow (u \cap B \subseteq x \land y \in u \land J ↾_{𝑡} (u \cap B) \in A))$
45	14 16 44	rexxfr2d	$⊢ (((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \to (\exists w \in (J ↾_{𝑡} B) (w \in 𝒫 z \land (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A)) \leftrightarrow \exists u \in J (u \cap B \subseteq x \land y \in u \land J ↾_{𝑡} (u \cap B) \in A))$
46	11 45	syl5bb	$⊢ (((J \in Top \land B \in V) \land z = x \cap B) \land y \in (x \cap B)) \to (\exists w \in ((J ↾_{𝑡} B) \cap 𝒫 z) (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A) \leftrightarrow \exists u \in J (u \cap B \subseteq x \land y \in u \land J ↾_{𝑡} (u \cap B) \in A))$
47	46	ralbidva	$⊢ ((J \in Top \land B \in V) \land z = x \cap B) \to (\forall y \in (x \cap B) \exists w \in ((J ↾_{𝑡} B) \cap 𝒫 z) (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A) \leftrightarrow \forall y \in (x \cap B) \exists u \in J (u \cap B \subseteq x \land y \in u \land J ↾_{𝑡} (u \cap B) \in A))$
48	10 47	bitrd	$⊢ ((J \in Top \land B \in V) \land z = x \cap B) \to (\forall y \in z \exists w \in ((J ↾_{𝑡} B) \cap 𝒫 z) (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A) \leftrightarrow \forall y \in (x \cap B) \exists u \in J (u \cap B \subseteq x \land y \in u \land J ↾_{𝑡} (u \cap B) \in A))$
49	7 8 48	ralxfr2d	$⊢ (J \in Top \land B \in V) \to (\forall z \in (J ↾_{𝑡} B) \forall y \in z \exists w \in ((J ↾_{𝑡} B) \cap 𝒫 z) (y \in w \land (J ↾_{𝑡} B) ↾_{𝑡} w \in A) \leftrightarrow \forall x \in J \forall y \in (x \cap B) \exists u \in J (u \cap B \subseteq x \land y \in u \land J ↾_{𝑡} (u \cap B) \in A))$
50	4 49	bitrd	$⊢ (J \in Top \land B \in V) \to (J ↾_{𝑡} B \in LocallyA\leftrightarrow\forall x \in J \forall y \in (x \cap B) \exists u \in J (u \cap B \subseteq x \land y \in u \land J ↾_{𝑡} (u \cap B) \in A))$

Metamath Proof Explorer

Theorem subislly

Proof