flimrest

Description: The set of limit points in a restricted topological space. (Contributed by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Assertion	flimrest	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (J ↾_{𝑡} Y) fLim (F ↾_{𝑡} Y) = (J fLim F) \cap Y$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to J \in TopOn (X)$
2		filelss	$⊢ (F \in Fil (X) \land Y \in F) \to Y \subseteq X$
3	2	3adant1	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to Y \subseteq X$
4		resttopon	$⊢ (J \in TopOn (X) \land Y \subseteq X) \to J ↾_{𝑡} Y \in TopOn (Y)$
5	1 3 4	syl2anc	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to J ↾_{𝑡} Y \in TopOn (Y)$
6		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
7	6	3ad2ant2	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to F \in fBas (X)$
8		simp3	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to Y \in F$
9		fbncp	$⊢ (F \in fBas (X) \land Y \in F) \to \neg X ∖ Y \in F$
10	7 8 9	syl2anc	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to \neg X ∖ Y \in F$
11		simp2	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to F \in Fil (X)$
12		trfil3	$⊢ (F \in Fil (X) \land Y \subseteq X) \to (F ↾_{𝑡} Y \in Fil (Y) \leftrightarrow \neg X ∖ Y \in F)$
13	11 3 12	syl2anc	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (F ↾_{𝑡} Y \in Fil (Y) \leftrightarrow \neg X ∖ Y \in F)$
14	10 13	mpbird	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to F ↾_{𝑡} Y \in Fil (Y)$
15		flimopn	$⊢ (J ↾_{𝑡} Y \in TopOn (Y) \land F ↾_{𝑡} Y \in Fil (Y)) \to (x \in ((J ↾_{𝑡} Y) fLim (F ↾_{𝑡} Y)) \leftrightarrow (x \in Y \land \forall y \in (J ↾_{𝑡} Y) (x \in y \to y \in (F ↾_{𝑡} Y))))$
16	5 14 15	syl2anc	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (x \in ((J ↾_{𝑡} Y) fLim (F ↾_{𝑡} Y)) \leftrightarrow (x \in Y \land \forall y \in (J ↾_{𝑡} Y) (x \in y \to y \in (F ↾_{𝑡} Y))))$
17		simpll2	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z \in J) \to F \in Fil (X)$
18		simpll3	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z \in J) \to Y \in F$
19		elrestr	$⊢ (F \in Fil (X) \land Y \in F \land z \in F) \to z \cap Y \in (F ↾_{𝑡} Y)$
20	19	3expia	$⊢ (F \in Fil (X) \land Y \in F) \to (z \in F \to z \cap Y \in (F ↾_{𝑡} Y))$
21	17 18 20	syl2anc	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z \in J) \to (z \in F \to z \cap Y \in (F ↾_{𝑡} Y))$
22		trfilss	$⊢ (F \in Fil (X) \land Y \in F) \to F ↾_{𝑡} Y \subseteq F$
23	17 18 22	syl2anc	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z \in J) \to F ↾_{𝑡} Y \subseteq F$
24	23	sseld	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z \in J) \to (z \cap Y \in (F ↾_{𝑡} Y) \to z \cap Y \in F)$
25		inss1	$⊢ z \cap Y \subseteq z$
26	25	a1i	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z \in J) \to z \cap Y \subseteq z$
27		simpl1	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to J \in TopOn (X)$
28		toponss	$⊢ (J \in TopOn (X) \land z \in J) \to z \subseteq X$
29	27 28	sylan	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z \in J) \to z \subseteq X$
30		filss	$⊢ (F \in Fil (X) \land (z \cap Y \in F \land z \subseteq X \land z \cap Y \subseteq z)) \to z \in F$
31	30	3exp2	$⊢ F \in Fil (X) \to (z \cap Y \in F \to (z \subseteq X \to (z \cap Y \subseteq z \to z \in F)))$
32	31	com24	$⊢ F \in Fil (X) \to (z \cap Y \subseteq z \to (z \subseteq X \to (z \cap Y \in F \to z \in F)))$
33	17 26 29 32	syl3c	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z \in J) \to (z \cap Y \in F \to z \in F)$
34	24 33	syld	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z \in J) \to (z \cap Y \in (F ↾_{𝑡} Y) \to z \in F)$
35	21 34	impbid	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z \in J) \to (z \in F \leftrightarrow z \cap Y \in (F ↾_{𝑡} Y))$
36	35	imbi2d	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z \in J) \to ((x \in z \to z \in F) \leftrightarrow (x \in z \to z \cap Y \in (F ↾_{𝑡} Y)))$
37	36	ralbidva	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to (\forall z \in J (x \in z \to z \in F) \leftrightarrow \forall z \in J (x \in z \to z \cap Y \in (F ↾_{𝑡} Y)))$
38		simpl2	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to F \in Fil (X)$
39	3	sselda	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to x \in X$
40		flimopn	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (x \in (J fLim F) \leftrightarrow (x \in X \land \forall z \in J (x \in z \to z \in F)))$
41	40	baibd	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land x \in X) \to (x \in (J fLim F) \leftrightarrow \forall z \in J (x \in z \to z \in F))$
42	27 38 39 41	syl21anc	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to (x \in (J fLim F) \leftrightarrow \forall z \in J (x \in z \to z \in F))$
43		vex	$⊢ z \in V$
44	43	inex1	$⊢ z \cap Y \in V$
45	44	a1i	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z \in J) \to z \cap Y \in V$
46		simpl3	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to Y \in F$
47		elrest	$⊢ (J \in TopOn (X) \land Y \in F) \to (y \in (J ↾_{𝑡} Y) \leftrightarrow \exists z \in J y = z \cap Y)$
48	27 46 47	syl2anc	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to (y \in (J ↾_{𝑡} Y) \leftrightarrow \exists z \in J y = z \cap Y)$
49		eleq2	$⊢ y = z \cap Y \to (x \in y \leftrightarrow x \in (z \cap Y))$
50		elin	$⊢ x \in (z \cap Y) \leftrightarrow (x \in z \land x \in Y)$
51	50	rbaib	$⊢ x \in Y \to (x \in (z \cap Y) \leftrightarrow x \in z)$
52	51	adantl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to (x \in (z \cap Y) \leftrightarrow x \in z)$
53	49 52	sylan9bbr	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land y = z \cap Y) \to (x \in y \leftrightarrow x \in z)$
54		eleq1	$⊢ y = z \cap Y \to (y \in (F ↾_{𝑡} Y) \leftrightarrow z \cap Y \in (F ↾_{𝑡} Y))$
55	54	adantl	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land y = z \cap Y) \to (y \in (F ↾_{𝑡} Y) \leftrightarrow z \cap Y \in (F ↾_{𝑡} Y))$
56	53 55	imbi12d	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land y = z \cap Y) \to ((x \in y \to y \in (F ↾_{𝑡} Y)) \leftrightarrow (x \in z \to z \cap Y \in (F ↾_{𝑡} Y)))$
57	45 48 56	ralxfr2d	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to (\forall y \in (J ↾_{𝑡} Y) (x \in y \to y \in (F ↾_{𝑡} Y)) \leftrightarrow \forall z \in J (x \in z \to z \cap Y \in (F ↾_{𝑡} Y)))$
58	37 42 57	3bitr4d	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to (x \in (J fLim F) \leftrightarrow \forall y \in (J ↾_{𝑡} Y) (x \in y \to y \in (F ↾_{𝑡} Y)))$
59	58	pm5.32da	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to ((x \in Y \land x \in (J fLim F)) \leftrightarrow (x \in Y \land \forall y \in (J ↾_{𝑡} Y) (x \in y \to y \in (F ↾_{𝑡} Y))))$
60	16 59	bitr4d	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (x \in ((J ↾_{𝑡} Y) fLim (F ↾_{𝑡} Y)) \leftrightarrow (x \in Y \land x \in (J fLim F)))$
61		ancom	$⊢ (x \in Y \land x \in (J fLim F)) \leftrightarrow (x \in (J fLim F) \land x \in Y)$
62		elin	$⊢ x \in ((J fLim F) \cap Y) \leftrightarrow (x \in (J fLim F) \land x \in Y)$
63	61 62	bitr4i	$⊢ (x \in Y \land x \in (J fLim F)) \leftrightarrow x \in ((J fLim F) \cap Y)$
64	60 63	bitrdi	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (x \in ((J ↾_{𝑡} Y) fLim (F ↾_{𝑡} Y)) \leftrightarrow x \in ((J fLim F) \cap Y))$
65	64	eqrdv	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (J ↾_{𝑡} Y) fLim (F ↾_{𝑡} Y) = (J fLim F) \cap Y$

Metamath Proof Explorer

Theorem flimrest

Proof