Metamath Proof Explorer

Theorem fgmin

Description: Minimality property of a generated filter: every filter that contains B contains its generated filter. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Mario Carneiro, 7-Aug-2015)

Ref Expression
Assertion fgmin 
|- ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) -> ( B C_ F <-> ( X filGen B ) C_ F ) )

Proof

Step Hyp Ref Expression
1 elfg 
 |-  ( B e. ( fBas ` X ) -> ( t e. ( X filGen B ) <-> ( t C_ X /\ E. x e. B x C_ t ) ) )
2 1 adantr 
 |-  ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) -> ( t e. ( X filGen B ) <-> ( t C_ X /\ E. x e. B x C_ t ) ) )
3 2 adantr 
 |-  ( ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) /\ B C_ F ) -> ( t e. ( X filGen B ) <-> ( t C_ X /\ E. x e. B x C_ t ) ) )
4 ssrexv 
 |-  ( B C_ F -> ( E. x e. B x C_ t -> E. x e. F x C_ t ) )
5 4 adantl 
 |-  ( ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) /\ B C_ F ) -> ( E. x e. B x C_ t -> E. x e. F x C_ t ) )
6 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( x e. F /\ t C_ X /\ x C_ t ) ) -> t e. F )
7 6 3exp2 
 |-  ( F e. ( Fil ` X ) -> ( x e. F -> ( t C_ X -> ( x C_ t -> t e. F ) ) ) )
8 7 com34 
 |-  ( F e. ( Fil ` X ) -> ( x e. F -> ( x C_ t -> ( t C_ X -> t e. F ) ) ) )
9 8 rexlimdv 
 |-  ( F e. ( Fil ` X ) -> ( E. x e. F x C_ t -> ( t C_ X -> t e. F ) ) )
10 9 ad2antlr 
 |-  ( ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) /\ B C_ F ) -> ( E. x e. F x C_ t -> ( t C_ X -> t e. F ) ) )
11 5 10 syld 
 |-  ( ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) /\ B C_ F ) -> ( E. x e. B x C_ t -> ( t C_ X -> t e. F ) ) )
12 11 com23 
 |-  ( ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) /\ B C_ F ) -> ( t C_ X -> ( E. x e. B x C_ t -> t e. F ) ) )
13 12 impd 
 |-  ( ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) /\ B C_ F ) -> ( ( t C_ X /\ E. x e. B x C_ t ) -> t e. F ) )
14 3 13 sylbid 
 |-  ( ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) /\ B C_ F ) -> ( t e. ( X filGen B ) -> t e. F ) )
15 14 ssrdv 
 |-  ( ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) /\ B C_ F ) -> ( X filGen B ) C_ F )
16 15 ex 
 |-  ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) -> ( B C_ F -> ( X filGen B ) C_ F ) )
17 ssfg 
 |-  ( B e. ( fBas ` X ) -> B C_ ( X filGen B ) )
18 sstr2 
 |-  ( B C_ ( X filGen B ) -> ( ( X filGen B ) C_ F -> B C_ F ) )
19 17 18 syl 
 |-  ( B e. ( fBas ` X ) -> ( ( X filGen B ) C_ F -> B C_ F ) )
20 19 adantr 
 |-  ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) -> ( ( X filGen B ) C_ F -> B C_ F ) )
21 16 20 impbid 
 |-  ( ( B e. ( fBas ` X ) /\ F e. ( Fil ` X ) ) -> ( B C_ F <-> ( X filGen B ) C_ F ) )