fclsval

Description: The set of all cluster points 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	fclsval	$⊢ (J \in Top \land F \in Fil (Y)) \to J fClus F = if (X = Y, ⋂_{t \in F} cls (J) (t), \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		fclsval.x	$⊢ X = ⋃ J$
2		simpl	$⊢ (J \in Top \land F \in Fil (Y)) \to J \in Top$
3		fvssunirn	$⊢ Fil (Y) \subseteq ⋃ ran Fil$
4	3	sseli	$⊢ F \in Fil (Y) \to F \in ⋃ ran Fil$
5	4	adantl	$⊢ (J \in Top \land F \in Fil (Y)) \to F \in ⋃ ran Fil$
6		filn0	$⊢ F \in Fil (Y) \to F \neq \emptyset$
7	6	adantl	$⊢ (J \in Top \land F \in Fil (Y)) \to F \neq \emptyset$
8		fvex	$⊢ cls (J) (t) \in V$
9	8	rgenw	$⊢ \forall t \in F cls (J) (t) \in V$
10		iinexg	$⊢ (F \neq \emptyset \land \forall t \in F cls (J) (t) \in V) \to ⋂_{t \in F} cls (J) (t) \in V$
11	7 9 10	sylancl	$⊢ (J \in Top \land F \in Fil (Y)) \to ⋂_{t \in F} cls (J) (t) \in V$
12		0ex	$⊢ \emptyset \in V$
13		ifcl	$⊢ (⋂_{t \in F} cls (J) (t) \in V \land \emptyset \in V) \to if (X = ⋃ F, ⋂_{t \in F} cls (J) (t), \emptyset) \in V$
14	11 12 13	sylancl	$⊢ (J \in Top \land F \in Fil (Y)) \to if (X = ⋃ F, ⋂_{t \in F} cls (J) (t), \emptyset) \in V$
15		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
16	15 1	syl6eqr	$⊢ j = J \to ⋃ j = X$
17		unieq	$⊢ f = F \to ⋃ f = ⋃ F$
18	16 17	eqeqan12d	$⊢ (j = J \land f = F) \to (⋃ j = ⋃ f \leftrightarrow X = ⋃ F)$
19		iineq1	$⊢ f = F \to ⋂_{t \in f} cls (j) (t) = ⋂_{t \in F} cls (j) (t)$
20	19	adantl	$⊢ (j = J \land f = F) \to ⋂_{t \in f} cls (j) (t) = ⋂_{t \in F} cls (j) (t)$
21		simpll	$⊢ ((j = J \land f = F) \land t \in F) \to j = J$
22	21	fveq2d	$⊢ ((j = J \land f = F) \land t \in F) \to cls (j) = cls (J)$
23	22	fveq1d	$⊢ ((j = J \land f = F) \land t \in F) \to cls (j) (t) = cls (J) (t)$
24	23	iineq2dv	$⊢ (j = J \land f = F) \to ⋂_{t \in F} cls (j) (t) = ⋂_{t \in F} cls (J) (t)$
25	20 24	eqtrd	$⊢ (j = J \land f = F) \to ⋂_{t \in f} cls (j) (t) = ⋂_{t \in F} cls (J) (t)$
26	18 25	ifbieq1d	$⊢ (j = J \land f = F) \to if (⋃ j = ⋃ f, ⋂_{t \in f} cls (j) (t), \emptyset) = if (X = ⋃ F, ⋂_{t \in F} cls (J) (t), \emptyset)$
27		df-fcls	$⊢ fClus = (j \in Top, f \in ⋃ ran Fil ⟼ if (⋃ j = ⋃ f, ⋂_{t \in f} cls (j) (t), \emptyset))$
28	26 27	ovmpoga	$⊢ (J \in Top \land F \in ⋃ ran Fil \land if (X = ⋃ F, ⋂_{t \in F} cls (J) (t), \emptyset) \in V) \to J fClus F = if (X = ⋃ F, ⋂_{t \in F} cls (J) (t), \emptyset)$
29	2 5 14 28	syl3anc	$⊢ (J \in Top \land F \in Fil (Y)) \to J fClus F = if (X = ⋃ F, ⋂_{t \in F} cls (J) (t), \emptyset)$
30		filunibas	$⊢ F \in Fil (Y) \to ⋃ F = Y$
31	30	eqeq2d	$⊢ F \in Fil (Y) \to (X = ⋃ F \leftrightarrow X = Y)$
32	31	adantl	$⊢ (J \in Top \land F \in Fil (Y)) \to (X = ⋃ F \leftrightarrow X = Y)$
33	32	ifbid	$⊢ (J \in Top \land F \in Fil (Y)) \to if (X = ⋃ F, ⋂_{t \in F} cls (J) (t), \emptyset) = if (X = Y, ⋂_{t \in F} cls (J) (t), \emptyset)$
34	29 33	eqtrd	$⊢ (J \in Top \land F \in Fil (Y)) \to J fClus F = if (X = Y, ⋂_{t \in F} cls (J) (t), \emptyset)$

Metamath Proof Explorer

Theorem fclsval

Proof