Metamath Proof Explorer

Theorem uffclsflim

Description: The cluster points of an ultrafilter are its limit points. (Contributed by Jeff Hankins, 11-Dec-2009) (Revised by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Assertion	uffclsflim	$⊢ F \in UFil (X) \to J fClus F = J fLim F$

Proof

Step	Hyp	Ref	Expression
1		ufilfil	$⊢ F \in UFil (X) \to F \in Fil (X)$
2		fclsfnflim	$⊢ F \in Fil (X) \to (x \in (J fClus F) \leftrightarrow \exists f \in Fil (X) (F \subseteq f \land x \in (J fLim f)))$
3	1 2	syl	$⊢ F \in UFil (X) \to (x \in (J fClus F) \leftrightarrow \exists f \in Fil (X) (F \subseteq f \land x \in (J fLim f)))$
4	3	biimpa	$⊢ (F \in UFil (X) \land x \in (J fClus F)) \to \exists f \in Fil (X) (F \subseteq f \land x \in (J fLim f))$
5		simprrr	$⊢ ((F \in UFil (X) \land x \in (J fClus F)) \land (f \in Fil (X) \land (F \subseteq f \land x \in (J fLim f)))) \to x \in (J fLim f)$
6		simpll	$⊢ ((F \in UFil (X) \land x \in (J fClus F)) \land (f \in Fil (X) \land (F \subseteq f \land x \in (J fLim f)))) \to F \in UFil (X)$
7		simprl	$⊢ ((F \in UFil (X) \land x \in (J fClus F)) \land (f \in Fil (X) \land (F \subseteq f \land x \in (J fLim f)))) \to f \in Fil (X)$
8		simprrl	$⊢ ((F \in UFil (X) \land x \in (J fClus F)) \land (f \in Fil (X) \land (F \subseteq f \land x \in (J fLim f)))) \to F \subseteq f$
9		ufilmax	$⊢ (F \in UFil (X) \land f \in Fil (X) \land F \subseteq f) \to F = f$
10	6 7 8 9	syl3anc	$⊢ ((F \in UFil (X) \land x \in (J fClus F)) \land (f \in Fil (X) \land (F \subseteq f \land x \in (J fLim f)))) \to F = f$
11	10	oveq2d	$⊢ ((F \in UFil (X) \land x \in (J fClus F)) \land (f \in Fil (X) \land (F \subseteq f \land x \in (J fLim f)))) \to J fLim F = J fLim f$
12	5 11	eleqtrrd	$⊢ ((F \in UFil (X) \land x \in (J fClus F)) \land (f \in Fil (X) \land (F \subseteq f \land x \in (J fLim f)))) \to x \in (J fLim F)$
13	4 12	rexlimddv	$⊢ (F \in UFil (X) \land x \in (J fClus F)) \to x \in (J fLim F)$
14	13	ex	$⊢ F \in UFil (X) \to (x \in (J fClus F) \to x \in (J fLim F))$
15	14	ssrdv	$⊢ F \in UFil (X) \to J fClus F \subseteq J fLim F$
16		flimfcls	$⊢ J fLim F \subseteq J fClus F$
17	16	a1i	$⊢ F \in UFil (X) \to J fLim F \subseteq J fClus F$
18	15 17	eqssd	$⊢ F \in UFil (X) \to J fClus F = J fLim F$