isfcls

Description: A cluster point of a filter. (Contributed by Jeff Hankins, 10-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

		Ref	Expression
	Hypothesis	fclsval.x	$⊢ X = ⋃ J$
	Assertion	isfcls	$⊢ A \in (J fClus F) \leftrightarrow (J \in Top \land F \in Fil (X) \land \forall s \in F A \in cls (J) (s))$

Proof

Step	Hyp	Ref	Expression
1		fclsval.x	$⊢ X = ⋃ J$
2		anass	$⊢ (((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \land \forall s \in F A \in cls (J) (s)) \leftrightarrow ((J \in Top \land F \in ⋃ ran Fil) \land (X = ⋃ F \land \forall s \in F A \in cls (J) (s)))$
3		fvssunirn	$⊢ Fil (X) \subseteq ⋃ ran Fil$
4	3	sseli	$⊢ F \in Fil (X) \to F \in ⋃ ran Fil$
5		filunibas	$⊢ F \in Fil (X) \to ⋃ F = X$
6	5	eqcomd	$⊢ F \in Fil (X) \to X = ⋃ F$
7	4 6	jca	$⊢ F \in Fil (X) \to (F \in ⋃ ran Fil \land X = ⋃ F)$
8		filunirn	$⊢ F \in ⋃ ran Fil \leftrightarrow F \in Fil (⋃ F)$
9		fveq2	$⊢ X = ⋃ F \to Fil (X) = Fil (⋃ F)$
10	9	eleq2d	$⊢ X = ⋃ F \to (F \in Fil (X) \leftrightarrow F \in Fil (⋃ F))$
11	10	biimparc	$⊢ (F \in Fil (⋃ F) \land X = ⋃ F) \to F \in Fil (X)$
12	8 11	sylanb	$⊢ (F \in ⋃ ran Fil \land X = ⋃ F) \to F \in Fil (X)$
13	7 12	impbii	$⊢ F \in Fil (X) \leftrightarrow (F \in ⋃ ran Fil \land X = ⋃ F)$
14	13	anbi2i	$⊢ (J \in Top \land F \in Fil (X)) \leftrightarrow (J \in Top \land (F \in ⋃ ran Fil \land X = ⋃ F))$
15	14	anbi1i	$⊢ ((J \in Top \land F \in Fil (X)) \land \forall s \in F A \in cls (J) (s)) \leftrightarrow ((J \in Top \land (F \in ⋃ ran Fil \land X = ⋃ F)) \land \forall s \in F A \in cls (J) (s))$
16		df-3an	$⊢ (J \in Top \land F \in Fil (X) \land \forall s \in F A \in cls (J) (s)) \leftrightarrow ((J \in Top \land F \in Fil (X)) \land \forall s \in F A \in cls (J) (s))$
17		anass	$⊢ ((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \leftrightarrow (J \in Top \land (F \in ⋃ ran Fil \land X = ⋃ F))$
18	17	anbi1i	$⊢ (((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \land \forall s \in F A \in cls (J) (s)) \leftrightarrow ((J \in Top \land (F \in ⋃ ran Fil \land X = ⋃ F)) \land \forall s \in F A \in cls (J) (s))$
19	15 16 18	3bitr4i	$⊢ (J \in Top \land F \in Fil (X) \land \forall s \in F A \in cls (J) (s)) \leftrightarrow (((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \land \forall s \in F A \in cls (J) (s))$
20		df-fcls	$⊢ fClus = (j \in Top, f \in ⋃ ran Fil ⟼ if (⋃ j = ⋃ f, ⋂_{x \in f} cls (j) (x), \emptyset))$
21	20	elmpocl	$⊢ A \in (J fClus F) \to (J \in Top \land F \in ⋃ ran Fil)$
22	1	fclsval	$⊢ (J \in Top \land F \in Fil (⋃ F)) \to J fClus F = if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset)$
23	8 22	sylan2b	$⊢ (J \in Top \land F \in ⋃ ran Fil) \to J fClus F = if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset)$
24	23	eleq2d	$⊢ (J \in Top \land F \in ⋃ ran Fil) \to (A \in (J fClus F) \leftrightarrow A \in if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset))$
25		n0i	$⊢ A \in if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset) \to \neg if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset) = \emptyset$
26		iffalse	$⊢ \neg X = ⋃ F \to if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset) = \emptyset$
27	25 26	nsyl2	$⊢ A \in if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset) \to X = ⋃ F$
28	27	a1i	$⊢ (J \in Top \land F \in ⋃ ran Fil) \to (A \in if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset) \to X = ⋃ F)$
29	28	pm4.71rd	$⊢ (J \in Top \land F \in ⋃ ran Fil) \to (A \in if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset) \leftrightarrow (X = ⋃ F \land A \in if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset)))$
30		iftrue	$⊢ X = ⋃ F \to if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset) = ⋂_{s \in F} cls (J) (s)$
31	30	adantl	$⊢ ((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \to if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset) = ⋂_{s \in F} cls (J) (s)$
32	31	eleq2d	$⊢ ((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \to (A \in if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset) \leftrightarrow A \in ⋂_{s \in F} cls (J) (s))$
33		elex	$⊢ A \in ⋂_{s \in F} cls (J) (s) \to A \in V$
34	33	a1i	$⊢ ((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \to (A \in ⋂_{s \in F} cls (J) (s) \to A \in V)$
35		filn0	$⊢ F \in Fil (⋃ F) \to F \neq \emptyset$
36	8 35	sylbi	$⊢ F \in ⋃ ran Fil \to F \neq \emptyset$
37	36	ad2antlr	$⊢ ((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \to F \neq \emptyset$
38		r19.2z	$⊢ (F \neq \emptyset \land \forall s \in F A \in cls (J) (s)) \to \exists s \in F A \in cls (J) (s)$
39	38	ex	$⊢ F \neq \emptyset \to (\forall s \in F A \in cls (J) (s) \to \exists s \in F A \in cls (J) (s))$
40	37 39	syl	$⊢ ((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \to (\forall s \in F A \in cls (J) (s) \to \exists s \in F A \in cls (J) (s))$
41		elex	$⊢ A \in cls (J) (s) \to A \in V$
42	41	rexlimivw	$⊢ \exists s \in F A \in cls (J) (s) \to A \in V$
43	40 42	syl6	$⊢ ((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \to (\forall s \in F A \in cls (J) (s) \to A \in V)$
44		eliin	$⊢ A \in V \to (A \in ⋂_{s \in F} cls (J) (s) \leftrightarrow \forall s \in F A \in cls (J) (s))$
45	44	a1i	$⊢ ((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \to (A \in V \to (A \in ⋂_{s \in F} cls (J) (s) \leftrightarrow \forall s \in F A \in cls (J) (s)))$
46	34 43 45	pm5.21ndd	$⊢ ((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \to (A \in ⋂_{s \in F} cls (J) (s) \leftrightarrow \forall s \in F A \in cls (J) (s))$
47	32 46	bitrd	$⊢ ((J \in Top \land F \in ⋃ ran Fil) \land X = ⋃ F) \to (A \in if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset) \leftrightarrow \forall s \in F A \in cls (J) (s))$
48	47	pm5.32da	$⊢ (J \in Top \land F \in ⋃ ran Fil) \to ((X = ⋃ F \land A \in if (X = ⋃ F, ⋂_{s \in F} cls (J) (s), \emptyset)) \leftrightarrow (X = ⋃ F \land \forall s \in F A \in cls (J) (s)))$
49	24 29 48	3bitrd	$⊢ (J \in Top \land F \in ⋃ ran Fil) \to (A \in (J fClus F) \leftrightarrow (X = ⋃ F \land \forall s \in F A \in cls (J) (s)))$
50	21 49	biadanii	$⊢ A \in (J fClus F) \leftrightarrow ((J \in Top \land F \in ⋃ ran Fil) \land (X = ⋃ F \land \forall s \in F A \in cls (J) (s)))$
51	2 19 50	3bitr4ri	$⊢ A \in (J fClus F) \leftrightarrow (J \in Top \land F \in Fil (X) \land \forall s \in F A \in cls (J) (s))$

Metamath Proof Explorer

Theorem isfcls

Proof