Theorem 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 e. ( Fil ` X ) -> ( X filGen F ) = F )

Proof

Step	Hyp	Ref	Expression
1		filfbas	|- ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
2		elfg	|- ( F e. ( fBas ` X ) -> ( t e. ( X filGen F ) <-> ( t C_ X /\ E. x e. F x C_ t ) ) )
3	1 2	syl	|- ( F e. ( Fil ` X ) -> ( t e. ( X filGen F ) <-> ( t C_ X /\ E. x e. F x C_ t ) ) )
4		filss	|- ( ( F e. ( Fil ` X ) /\ ( x e. F /\ t C_ X /\ x C_ t ) ) -> t e. F )
5	4	3exp2	|- ( F e. ( Fil ` X ) -> ( x e. F -> ( t C_ X -> ( x C_ t -> t e. F ) ) ) )
6	5	com34	|- ( F e. ( Fil ` X ) -> ( x e. F -> ( x C_ t -> ( t C_ X -> t e. F ) ) ) )
7	6	rexlimdv	|- ( F e. ( Fil ` X ) -> ( E. x e. F x C_ t -> ( t C_ X -> t e. F ) ) )
8	7	impcomd	|- ( F e. ( Fil ` X ) -> ( ( t C_ X /\ E. x e. F x C_ t ) -> t e. F ) )
9	3 8	sylbid	|- ( F e. ( Fil ` X ) -> ( t e. ( X filGen F ) -> t e. F ) )
10	9	ssrdv	|- ( F e. ( Fil ` X ) -> ( X filGen F ) C_ F )
11		ssfg	|- ( F e. ( fBas ` X ) -> F C_ ( X filGen F ) )
12	1 11	syl	|- ( F e. ( Fil ` X ) -> F C_ ( X filGen F ) )
13	10 12	eqssd	|- ( F e. ( Fil ` X ) -> ( X filGen F ) = F )