fclsrest

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

		Ref	Expression
	Assertion	fclsrest	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (J ↾_{𝑡} Y) fClus (F ↾_{𝑡} Y) = (J fClus 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		fclsopn	$⊢ (J ↾_{𝑡} Y \in TopOn (Y) \land F ↾_{𝑡} Y \in Fil (Y)) \to (x \in ((J ↾_{𝑡} Y) fClus (F ↾_{𝑡} Y)) \leftrightarrow (x \in Y \land \forall y \in (J ↾_{𝑡} Y) (x \in y \to \forall z \in (F ↾_{𝑡} Y) y \cap z \neq \emptyset)))$
16	5 14 15	syl2anc	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (x \in ((J ↾_{𝑡} Y) fClus (F ↾_{𝑡} Y)) \leftrightarrow (x \in Y \land \forall y \in (J ↾_{𝑡} Y) (x \in y \to \forall z \in (F ↾_{𝑡} Y) y \cap z \neq \emptyset)))$
17		in32	$⊢ (u \cap s) \cap Y = (u \cap Y) \cap s$
18		ineq2	$⊢ s = t \to (u \cap Y) \cap s = (u \cap Y) \cap t$
19	17 18	eqtrid	$⊢ s = t \to (u \cap s) \cap Y = (u \cap Y) \cap t$
20	19	neeq1d	$⊢ s = t \to ((u \cap s) \cap Y \neq \emptyset \leftrightarrow (u \cap Y) \cap t \neq \emptyset)$
21	20	rspccv	$⊢ \forall s \in F (u \cap s) \cap Y \neq \emptyset \to (t \in F \to (u \cap Y) \cap t \neq \emptyset)$
22		inss1	$⊢ u \cap Y \subseteq u$
23		ssrin	$⊢ u \cap Y \subseteq u \to (u \cap Y) \cap t \subseteq u \cap t$
24	22 23	ax-mp	$⊢ (u \cap Y) \cap t \subseteq u \cap t$
25		ssn0	$⊢ ((u \cap Y) \cap t \subseteq u \cap t \land (u \cap Y) \cap t \neq \emptyset) \to u \cap t \neq \emptyset$
26	24 25	mpan	$⊢ (u \cap Y) \cap t \neq \emptyset \to u \cap t \neq \emptyset$
27	21 26	syl6	$⊢ \forall s \in F (u \cap s) \cap Y \neq \emptyset \to (t \in F \to u \cap t \neq \emptyset)$
28	27	ralrimiv	$⊢ \forall s \in F (u \cap s) \cap Y \neq \emptyset \to \forall t \in F u \cap t \neq \emptyset$
29	11	ad3antrrr	$⊢ ((((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land u \in J) \land s \in F) \to F \in Fil (X)$
30		simpr	$⊢ ((((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land u \in J) \land s \in F) \to s \in F$
31	8	ad3antrrr	$⊢ ((((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land u \in J) \land s \in F) \to Y \in F$
32		filin	$⊢ (F \in Fil (X) \land s \in F \land Y \in F) \to s \cap Y \in F$
33	29 30 31 32	syl3anc	$⊢ ((((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land u \in J) \land s \in F) \to s \cap Y \in F$
34		ineq2	$⊢ t = s \cap Y \to u \cap t = u \cap (s \cap Y)$
35		inass	$⊢ (u \cap s) \cap Y = u \cap (s \cap Y)$
36	34 35	eqtr4di	$⊢ t = s \cap Y \to u \cap t = (u \cap s) \cap Y$
37	36	neeq1d	$⊢ t = s \cap Y \to (u \cap t \neq \emptyset \leftrightarrow (u \cap s) \cap Y \neq \emptyset)$
38	37	rspcv	$⊢ s \cap Y \in F \to (\forall t \in F u \cap t \neq \emptyset \to (u \cap s) \cap Y \neq \emptyset)$
39	33 38	syl	$⊢ ((((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land u \in J) \land s \in F) \to (\forall t \in F u \cap t \neq \emptyset \to (u \cap s) \cap Y \neq \emptyset)$
40	39	ralrimdva	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land u \in J) \to (\forall t \in F u \cap t \neq \emptyset \to \forall s \in F (u \cap s) \cap Y \neq \emptyset)$
41	28 40	impbid2	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land u \in J) \to (\forall s \in F (u \cap s) \cap Y \neq \emptyset \leftrightarrow \forall t \in F u \cap t \neq \emptyset)$
42	41	imbi2d	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land u \in J) \to ((x \in u \to \forall s \in F (u \cap s) \cap Y \neq \emptyset) \leftrightarrow (x \in u \to \forall t \in F u \cap t \neq \emptyset))$
43	42	ralbidva	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to (\forall u \in J (x \in u \to \forall s \in F (u \cap s) \cap Y \neq \emptyset) \leftrightarrow \forall u \in J (x \in u \to \forall t \in F u \cap t \neq \emptyset))$
44		vex	$⊢ u \in V$
45	44	inex1	$⊢ u \cap Y \in V$
46	45	a1i	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land u \in J) \to u \cap Y \in V$
47		elrest	$⊢ (J \in TopOn (X) \land Y \in F) \to (y \in (J ↾_{𝑡} Y) \leftrightarrow \exists u \in J y = u \cap Y)$
48	47	3adant2	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (y \in (J ↾_{𝑡} Y) \leftrightarrow \exists u \in J y = u \cap Y)$
49	48	adantr	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to (y \in (J ↾_{𝑡} Y) \leftrightarrow \exists u \in J y = u \cap Y)$
50		eleq2	$⊢ y = u \cap Y \to (x \in y \leftrightarrow x \in (u \cap Y))$
51		elin	$⊢ x \in (u \cap Y) \leftrightarrow (x \in u \land x \in Y)$
52	51	rbaib	$⊢ x \in Y \to (x \in (u \cap Y) \leftrightarrow x \in u)$
53	52	adantl	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to (x \in (u \cap Y) \leftrightarrow x \in u)$
54	50 53	sylan9bbr	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land y = u \cap Y) \to (x \in y \leftrightarrow x \in u)$
55		vex	$⊢ s \in V$
56	55	inex1	$⊢ s \cap Y \in V$
57	56	a1i	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land s \in F) \to s \cap Y \in V$
58		elrest	$⊢ (F \in Fil (X) \land Y \in F) \to (z \in (F ↾_{𝑡} Y) \leftrightarrow \exists s \in F z = s \cap Y)$
59	58	3adant1	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (z \in (F ↾_{𝑡} Y) \leftrightarrow \exists s \in F z = s \cap Y)$
60	59	adantr	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to (z \in (F ↾_{𝑡} Y) \leftrightarrow \exists s \in F z = s \cap Y)$
61		ineq2	$⊢ z = s \cap Y \to y \cap z = y \cap (s \cap Y)$
62	61	adantl	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z = s \cap Y) \to y \cap z = y \cap (s \cap Y)$
63	62	neeq1d	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land z = s \cap Y) \to (y \cap z \neq \emptyset \leftrightarrow y \cap (s \cap Y) \neq \emptyset)$
64	57 60 63	ralxfr2d	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to (\forall z \in (F ↾_{𝑡} Y) y \cap z \neq \emptyset \leftrightarrow \forall s \in F y \cap (s \cap Y) \neq \emptyset)$
65		ineq1	$⊢ y = u \cap Y \to y \cap (s \cap Y) = (u \cap Y) \cap (s \cap Y)$
66		inindir	$⊢ (u \cap s) \cap Y = (u \cap Y) \cap (s \cap Y)$
67	65 66	eqtr4di	$⊢ y = u \cap Y \to y \cap (s \cap Y) = (u \cap s) \cap Y$
68	67	neeq1d	$⊢ y = u \cap Y \to (y \cap (s \cap Y) \neq \emptyset \leftrightarrow (u \cap s) \cap Y \neq \emptyset)$
69	68	ralbidv	$⊢ y = u \cap Y \to (\forall s \in F y \cap (s \cap Y) \neq \emptyset \leftrightarrow \forall s \in F (u \cap s) \cap Y \neq \emptyset)$
70	64 69	sylan9bb	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land y = u \cap Y) \to (\forall z \in (F ↾_{𝑡} Y) y \cap z \neq \emptyset \leftrightarrow \forall s \in F (u \cap s) \cap Y \neq \emptyset)$
71	54 70	imbi12d	$⊢ (((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \land y = u \cap Y) \to ((x \in y \to \forall z \in (F ↾_{𝑡} Y) y \cap z \neq \emptyset) \leftrightarrow (x \in u \to \forall s \in F (u \cap s) \cap Y \neq \emptyset))$
72	46 49 71	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 \forall z \in (F ↾_{𝑡} Y) y \cap z \neq \emptyset) \leftrightarrow \forall u \in J (x \in u \to \forall s \in F (u \cap s) \cap Y \neq \emptyset))$
73	1	adantr	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to J \in TopOn (X)$
74	11	adantr	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to F \in Fil (X)$
75	3	sselda	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to x \in X$
76		fclsopn	$⊢ (J \in TopOn (X) \land F \in Fil (X)) \to (x \in (J fClus F) \leftrightarrow (x \in X \land \forall u \in J (x \in u \to \forall t \in F u \cap t \neq \emptyset)))$
77	76	baibd	$⊢ ((J \in TopOn (X) \land F \in Fil (X)) \land x \in X) \to (x \in (J fClus F) \leftrightarrow \forall u \in J (x \in u \to \forall t \in F u \cap t \neq \emptyset))$
78	73 74 75 77	syl21anc	$⊢ ((J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \land x \in Y) \to (x \in (J fClus F) \leftrightarrow \forall u \in J (x \in u \to \forall t \in F u \cap t \neq \emptyset))$
79	43 72 78	3bitr4d	$⊢ ((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 \forall z \in (F ↾_{𝑡} Y) y \cap z \neq \emptyset) \leftrightarrow x \in (J fClus F))$
80	79	pm5.32da	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to ((x \in Y \land \forall y \in (J ↾_{𝑡} Y) (x \in y \to \forall z \in (F ↾_{𝑡} Y) y \cap z \neq \emptyset)) \leftrightarrow (x \in Y \land x \in (J fClus F)))$
81	16 80	bitrd	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (x \in ((J ↾_{𝑡} Y) fClus (F ↾_{𝑡} Y)) \leftrightarrow (x \in Y \land x \in (J fClus F)))$
82		elin	$⊢ x \in ((J fClus F) \cap Y) \leftrightarrow (x \in (J fClus F) \land x \in Y)$
83	82	biancomi	$⊢ x \in ((J fClus F) \cap Y) \leftrightarrow (x \in Y \land x \in (J fClus F))$
84	81 83	bitr4di	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (x \in ((J ↾_{𝑡} Y) fClus (F ↾_{𝑡} Y)) \leftrightarrow x \in ((J fClus F) \cap Y))$
85	84	eqrdv	$⊢ (J \in TopOn (X) \land F \in Fil (X) \land Y \in F) \to (J ↾_{𝑡} Y) fClus (F ↾_{𝑡} Y) = (J fClus F) \cap Y$

Metamath Proof Explorer

Theorem fclsrest

Proof