fgfil

Description: A filter generates itself. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	fgfil	$⊢ F \in Fil (X) \to X filGen F = F$

Step	Hyp	Ref	Expression
1		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
2		elfg	$⊢ F \in fBas (X) \to (t \in (X filGen F) \leftrightarrow (t \subseteq X \land \exists x \in F x \subseteq t))$
3	1 2	syl	$⊢ F \in Fil (X) \to (t \in (X filGen F) \leftrightarrow (t \subseteq X \land \exists x \in F x \subseteq t))$
4		filss	$⊢ (F \in Fil (X) \land (x \in F \land t \subseteq X \land x \subseteq t)) \to t \in F$
5	4	3exp2	$⊢ F \in Fil (X) \to (x \in F \to (t \subseteq X \to (x \subseteq t \to t \in F)))$
6	5	com34	$⊢ F \in Fil (X) \to (x \in F \to (x \subseteq t \to (t \subseteq X \to t \in F)))$
7	6	rexlimdv	$⊢ F \in Fil (X) \to (\exists x \in F x \subseteq t \to (t \subseteq X \to t \in F))$
8	7	impcomd	$⊢ F \in Fil (X) \to ((t \subseteq X \land \exists x \in F x \subseteq t) \to t \in F)$
9	3 8	sylbid	$⊢ F \in Fil (X) \to (t \in (X filGen F) \to t \in F)$
10	9	ssrdv	$⊢ F \in Fil (X) \to X filGen F \subseteq F$
11		ssfg	$⊢ F \in fBas (X) \to F \subseteq X filGen F$
12	1 11	syl	$⊢ F \in Fil (X) \to F \subseteq X filGen F$
13	10 12	eqssd	$⊢ F \in Fil (X) \to X filGen F = F$

Metamath Proof Explorer