islly2

Description: An alternative expression for J e. Locally A when A passes to open subspaces: A space is locally A if every point is contained in an open neighborhood with property A . (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Hypotheses	restlly.1	$⊢ (φ \land (j \in A \land x \in j)) \to j ↾_{𝑡} x \in A$
	islly2.2	$⊢ X = ⋃ J$
Assertion	islly2	$⊢ φ \to (J \in LocallyA\leftrightarrow(J \in Top \land \forall y \in X \exists u \in J (y \in u \land J ↾_{𝑡} u \in A)))$

Proof

Step	Hyp	Ref	Expression
1		restlly.1	$⊢ (φ \land (j \in A \land x \in j)) \to j ↾_{𝑡} x \in A$
2		islly2.2	$⊢ X = ⋃ J$
3		llytop	$⊢ J \in LocallyA\toJ \in Top$
4	3	adantl	$⊢ (φ \land J \in LocallyA\toJ \in Top)$
5		simplr	$⊢ ((φ \land J \in LocallyA\landy \in X\toJ \in LocallyA))$
6	4	adantr	$⊢ ((φ \land J \in LocallyA\landy \in X\toJ \in Top))$
7	2	topopn	$⊢ J \in Top \to X \in J$
8	6 7	syl	$⊢ ((φ \land J \in LocallyA\landy \in X\toX \in J))$
9		simpr	$⊢ ((φ \land J \in LocallyA\landy \in X\toy \in X))$
10		llyi	$⊢ (J \in LocallyA\landX \in J\landy \in X\to\exists u \in J (u \subseteq X \land y \in u \land J ↾_{𝑡} u \in A))$
11	5 8 9 10	syl3anc	$⊢ ((φ \land J \in LocallyA\landy \in X\to\exists u \in J (u \subseteq X \land y \in u \land J ↾_{𝑡} u \in A)))$
12		3simpc	$⊢ (u \subseteq X \land y \in u \land J ↾_{𝑡} u \in A) \to (y \in u \land J ↾_{𝑡} u \in A)$
13	12	reximi	$⊢ \exists u \in J (u \subseteq X \land y \in u \land J ↾_{𝑡} u \in A) \to \exists u \in J (y \in u \land J ↾_{𝑡} u \in A)$
14	11 13	syl	$⊢ ((φ \land J \in LocallyA\landy \in X\to\exists u \in J (y \in u \land J ↾_{𝑡} u \in A)))$
15	14	ralrimiva	$⊢ (φ \land J \in LocallyA\to\forall y \in X \exists u \in J (y \in u \land J ↾_{𝑡} u \in A))$
16	4 15	jca	$⊢ (φ \land J \in LocallyA\to(J \in Top \land \forall y \in X \exists u \in J (y \in u \land J ↾_{𝑡} u \in A)))$
17		simprl	$⊢ (φ \land (J \in Top \land \forall y \in X \exists u \in J (y \in u \land J ↾_{𝑡} u \in A))) \to J \in Top$
18		elssuni	$⊢ z \in J \to z \subseteq ⋃ J$
19	18 2	sseqtrrdi	$⊢ z \in J \to z \subseteq X$
20	19	adantl	$⊢ ((φ \land J \in Top) \land z \in J) \to z \subseteq X$
21		ssralv	$⊢ z \subseteq X \to (\forall y \in X \exists u \in J (y \in u \land J ↾_{𝑡} u \in A) \to \forall y \in z \exists u \in J (y \in u \land J ↾_{𝑡} u \in A))$
22	20 21	syl	$⊢ ((φ \land J \in Top) \land z \in J) \to (\forall y \in X \exists u \in J (y \in u \land J ↾_{𝑡} u \in A) \to \forall y \in z \exists u \in J (y \in u \land J ↾_{𝑡} u \in A))$
23		simpllr	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to J \in Top$
24		simplrl	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to z \in J$
25		simprl	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to u \in J$
26		inopn	$⊢ (J \in Top \land z \in J \land u \in J) \to z \cap u \in J$
27	23 24 25 26	syl3anc	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to z \cap u \in J$
28		vex	$⊢ z \in V$
29		inss1	$⊢ z \cap u \subseteq z$
30	28 29	elpwi2	$⊢ z \cap u \in 𝒫 z$
31	30	a1i	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to z \cap u \in 𝒫 z$
32	27 31	elind	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to z \cap u \in (J \cap 𝒫 z)$
33		simplrr	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to y \in z$
34		simprrl	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to y \in u$
35	33 34	elind	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to y \in (z \cap u)$
36		inss2	$⊢ z \cap u \subseteq u$
37	36	a1i	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to z \cap u \subseteq u$
38		restabs	$⊢ (J \in Top \land z \cap u \subseteq u \land u \in J) \to (J ↾_{𝑡} u) ↾_{𝑡} (z \cap u) = J ↾_{𝑡} (z \cap u)$
39	23 37 25 38	syl3anc	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to (J ↾_{𝑡} u) ↾_{𝑡} (z \cap u) = J ↾_{𝑡} (z \cap u)$
40		oveq2	$⊢ x = z \cap u \to (J ↾_{𝑡} u) ↾_{𝑡} x = (J ↾_{𝑡} u) ↾_{𝑡} (z \cap u)$
41	40	eleq1d	$⊢ x = z \cap u \to ((J ↾_{𝑡} u) ↾_{𝑡} x \in A \leftrightarrow (J ↾_{𝑡} u) ↾_{𝑡} (z \cap u) \in A)$
42		oveq1	$⊢ j = J ↾_{𝑡} u \to j ↾_{𝑡} x = (J ↾_{𝑡} u) ↾_{𝑡} x$
43	42	eleq1d	$⊢ j = J ↾_{𝑡} u \to (j ↾_{𝑡} x \in A \leftrightarrow (J ↾_{𝑡} u) ↾_{𝑡} x \in A)$
44	43	raleqbi1dv	$⊢ j = J ↾_{𝑡} u \to (\forall x \in j j ↾_{𝑡} x \in A \leftrightarrow \forall x \in (J ↾_{𝑡} u) (J ↾_{𝑡} u) ↾_{𝑡} x \in A)$
45	1	ralrimivva	$⊢ φ \to \forall j \in A \forall x \in j j ↾_{𝑡} x \in A$
46	45	ad3antrrr	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to \forall j \in A \forall x \in j j ↾_{𝑡} x \in A$
47		simprrr	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to J ↾_{𝑡} u \in A$
48	44 46 47	rspcdva	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to \forall x \in (J ↾_{𝑡} u) (J ↾_{𝑡} u) ↾_{𝑡} x \in A$
49		elrestr	$⊢ (J \in Top \land u \in J \land z \in J) \to z \cap u \in (J ↾_{𝑡} u)$
50	23 25 24 49	syl3anc	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to z \cap u \in (J ↾_{𝑡} u)$
51	41 48 50	rspcdva	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to (J ↾_{𝑡} u) ↾_{𝑡} (z \cap u) \in A$
52	39 51	eqeltrrd	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to J ↾_{𝑡} (z \cap u) \in A$
53		eleq2	$⊢ v = z \cap u \to (y \in v \leftrightarrow y \in (z \cap u))$
54		oveq2	$⊢ v = z \cap u \to J ↾_{𝑡} v = J ↾_{𝑡} (z \cap u)$
55	54	eleq1d	$⊢ v = z \cap u \to (J ↾_{𝑡} v \in A \leftrightarrow J ↾_{𝑡} (z \cap u) \in A)$
56	53 55	anbi12d	$⊢ v = z \cap u \to ((y \in v \land J ↾_{𝑡} v \in A) \leftrightarrow (y \in (z \cap u) \land J ↾_{𝑡} (z \cap u) \in A))$
57	56	rspcev	$⊢ (z \cap u \in (J \cap 𝒫 z) \land (y \in (z \cap u) \land J ↾_{𝑡} (z \cap u) \in A)) \to \exists v \in (J \cap 𝒫 z) (y \in v \land J ↾_{𝑡} v \in A)$
58	32 35 52 57	syl12anc	$⊢ (((φ \land J \in Top) \land (z \in J \land y \in z)) \land (u \in J \land (y \in u \land J ↾_{𝑡} u \in A))) \to \exists v \in (J \cap 𝒫 z) (y \in v \land J ↾_{𝑡} v \in A)$
59	58	rexlimdvaa	$⊢ ((φ \land J \in Top) \land (z \in J \land y \in z)) \to (\exists u \in J (y \in u \land J ↾_{𝑡} u \in A) \to \exists v \in (J \cap 𝒫 z) (y \in v \land J ↾_{𝑡} v \in A))$
60	59	anassrs	$⊢ (((φ \land J \in Top) \land z \in J) \land y \in z) \to (\exists u \in J (y \in u \land J ↾_{𝑡} u \in A) \to \exists v \in (J \cap 𝒫 z) (y \in v \land J ↾_{𝑡} v \in A))$
61	60	ralimdva	$⊢ ((φ \land J \in Top) \land z \in J) \to (\forall y \in z \exists u \in J (y \in u \land J ↾_{𝑡} u \in A) \to \forall y \in z \exists v \in (J \cap 𝒫 z) (y \in v \land J ↾_{𝑡} v \in A))$
62	22 61	syld	$⊢ ((φ \land J \in Top) \land z \in J) \to (\forall y \in X \exists u \in J (y \in u \land J ↾_{𝑡} u \in A) \to \forall y \in z \exists v \in (J \cap 𝒫 z) (y \in v \land J ↾_{𝑡} v \in A))$
63	62	ralrimdva	$⊢ (φ \land J \in Top) \to (\forall y \in X \exists u \in J (y \in u \land J ↾_{𝑡} u \in A) \to \forall z \in J \forall y \in z \exists v \in (J \cap 𝒫 z) (y \in v \land J ↾_{𝑡} v \in A))$
64	63	impr	$⊢ (φ \land (J \in Top \land \forall y \in X \exists u \in J (y \in u \land J ↾_{𝑡} u \in A))) \to \forall z \in J \forall y \in z \exists v \in (J \cap 𝒫 z) (y \in v \land J ↾_{𝑡} v \in A)$
65		islly	$⊢ J \in LocallyA\leftrightarrow(J \in Top \land \forall z \in J \forall y \in z \exists v \in (J \cap 𝒫 z) (y \in v \land J ↾_{𝑡} v \in A))$
66	17 64 65	sylanbrc	$⊢ (φ \land (J \in Top \land \forall y \in X \exists u \in J (y \in u \land J ↾_{𝑡} u \in A))) \to J \in LocallyA$
67	16 66	impbida	$⊢ φ \to (J \in LocallyA\leftrightarrow(J \in Top \land \forall y \in X \exists u \in J (y \in u \land J ↾_{𝑡} u \in A)))$

Metamath Proof Explorer

Theorem islly2

Proof