Metamath Proof Explorer

Theorem elfilss

Description: An element belongs to a filter iff any element below it does. (Contributed by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion elfilss ⊢ F ∈ Fil ⁡ X ∧ A ⊆ X → A ∈ F ↔ ∃ t ∈ F t ⊆ A

Proof

Step Hyp Ref Expression
1 ibar ⊢ A ⊆ X → ∃ t ∈ F t ⊆ A ↔ A ⊆ X ∧ ∃ t ∈ F t ⊆ A
2 1 adantl ⊢ F ∈ Fil ⁡ X ∧ A ⊆ X → ∃ t ∈ F t ⊆ A ↔ A ⊆ X ∧ ∃ t ∈ F t ⊆ A
3 filfbas ⊢ F ∈ Fil ⁡ X → F ∈ fBas ⁡ X
4 elfg ⊢ F ∈ fBas ⁡ X → A ∈ X filGen F ↔ A ⊆ X ∧ ∃ t ∈ F t ⊆ A
5 3 4 syl ⊢ F ∈ Fil ⁡ X → A ∈ X filGen F ↔ A ⊆ X ∧ ∃ t ∈ F t ⊆ A
6 5 adantr ⊢ F ∈ Fil ⁡ X ∧ A ⊆ X → A ∈ X filGen F ↔ A ⊆ X ∧ ∃ t ∈ F t ⊆ A
7 fgfil ⊢ F ∈ Fil ⁡ X → X filGen F = F
8 7 eleq2d ⊢ F ∈ Fil ⁡ X → A ∈ X filGen F ↔ A ∈ F
9 8 adantr ⊢ F ∈ Fil ⁡ X ∧ A ⊆ X → A ∈ X filGen F ↔ A ∈ F
10 2 6 9 3bitr2rd ⊢ F ∈ Fil ⁡ X ∧ A ⊆ X → A ∈ F ↔ ∃ t ∈ F t ⊆ A