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 ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X → B ⊆ F ↔ X filGen B ⊆ F

Proof

Step Hyp Ref Expression
1 elfg ⊢ B ∈ fBas ⁡ X → t ∈ X filGen B ↔ t ⊆ X ∧ ∃ x ∈ B x ⊆ t
2 1 adantr ⊢ B ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X → t ∈ X filGen B ↔ t ⊆ X ∧ ∃ x ∈ B x ⊆ t
3 2 adantr ⊢ B ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X ∧ B ⊆ F → t ∈ X filGen B ↔ t ⊆ X ∧ ∃ x ∈ B x ⊆ t
4 ssrexv ⊢ B ⊆ F → ∃ x ∈ B x ⊆ t → ∃ x ∈ F x ⊆ t
5 4 adantl ⊢ B ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X ∧ B ⊆ F → ∃ x ∈ B x ⊆ t → ∃ x ∈ F x ⊆ t
6 filss ⊢ F ∈ Fil ⁡ X ∧ x ∈ F ∧ t ⊆ X ∧ x ⊆ t → t ∈ F
7 6 3exp2 ⊢ F ∈ Fil ⁡ X → x ∈ F → t ⊆ X → x ⊆ t → t ∈ F
8 7 com34 ⊢ F ∈ Fil ⁡ X → x ∈ F → x ⊆ t → t ⊆ X → t ∈ F
9 8 rexlimdv ⊢ F ∈ Fil ⁡ X → ∃ x ∈ F x ⊆ t → t ⊆ X → t ∈ F
10 9 ad2antlr ⊢ B ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X ∧ B ⊆ F → ∃ x ∈ F x ⊆ t → t ⊆ X → t ∈ F
11 5 10 syld ⊢ B ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X ∧ B ⊆ F → ∃ x ∈ B x ⊆ t → t ⊆ X → t ∈ F
12 11 com23 ⊢ B ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X ∧ B ⊆ F → t ⊆ X → ∃ x ∈ B x ⊆ t → t ∈ F
13 12 impd ⊢ B ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X ∧ B ⊆ F → t ⊆ X ∧ ∃ x ∈ B x ⊆ t → t ∈ F
14 3 13 sylbid ⊢ B ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X ∧ B ⊆ F → t ∈ X filGen B → t ∈ F
15 14 ssrdv ⊢ B ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X ∧ B ⊆ F → X filGen B ⊆ F
16 15 ex ⊢ B ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X → B ⊆ F → X filGen B ⊆ F
17 ssfg ⊢ B ∈ fBas ⁡ X → B ⊆ X filGen B
18 sstr2 ⊢ B ⊆ X filGen B → X filGen B ⊆ F → B ⊆ F
19 17 18 syl ⊢ B ∈ fBas ⁡ X → X filGen B ⊆ F → B ⊆ F
20 19 adantr ⊢ B ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X → X filGen B ⊆ F → B ⊆ F
21 16 20 impbid ⊢ B ∈ fBas ⁡ X ∧ F ∈ Fil ⁡ X → B ⊆ F ↔ X filGen B ⊆ F