Metamath Proof Explorer

Theorem elfg

Description: A condition for elements of a generated filter. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion elfg ⊢ F ∈ fBas ⁡ X → A ∈ X filGen F ↔ A ⊆ X ∧ ∃ x ∈ F x ⊆ A

Proof

Step Hyp Ref Expression
1 fgval ⊢ F ∈ fBas ⁡ X → X filGen F = y ∈ 𝒫 X | F ∩ 𝒫 y ≠ ∅
2 1 eleq2d ⊢ F ∈ fBas ⁡ X → A ∈ X filGen F ↔ A ∈ y ∈ 𝒫 X | F ∩ 𝒫 y ≠ ∅
3 pweq ⊢ y = A → 𝒫 y = 𝒫 A
4 3 ineq2d ⊢ y = A → F ∩ 𝒫 y = F ∩ 𝒫 A
5 4 neeq1d ⊢ y = A → F ∩ 𝒫 y ≠ ∅ ↔ F ∩ 𝒫 A ≠ ∅
6 5 elrab ⊢ A ∈ y ∈ 𝒫 X | F ∩ 𝒫 y ≠ ∅ ↔ A ∈ 𝒫 X ∧ F ∩ 𝒫 A ≠ ∅
7 elfvdm ⊢ F ∈ fBas ⁡ X → X ∈ dom ⁡ fBas
8 elpw2g ⊢ X ∈ dom ⁡ fBas → A ∈ 𝒫 X ↔ A ⊆ X
9 7 8 syl ⊢ F ∈ fBas ⁡ X → A ∈ 𝒫 X ↔ A ⊆ X
10 elin ⊢ x ∈ F ∩ 𝒫 A ↔ x ∈ F ∧ x ∈ 𝒫 A
11 velpw ⊢ x ∈ 𝒫 A ↔ x ⊆ A
12 11 anbi2i ⊢ x ∈ F ∧ x ∈ 𝒫 A ↔ x ∈ F ∧ x ⊆ A
13 10 12 bitri ⊢ x ∈ F ∩ 𝒫 A ↔ x ∈ F ∧ x ⊆ A
14 13 exbii ⊢ ∃ x x ∈ F ∩ 𝒫 A ↔ ∃ x x ∈ F ∧ x ⊆ A
15 n0 ⊢ F ∩ 𝒫 A ≠ ∅ ↔ ∃ x x ∈ F ∩ 𝒫 A
16 df-rex ⊢ ∃ x ∈ F x ⊆ A ↔ ∃ x x ∈ F ∧ x ⊆ A
17 14 15 16 3bitr4i ⊢ F ∩ 𝒫 A ≠ ∅ ↔ ∃ x ∈ F x ⊆ A
18 17 a1i ⊢ F ∈ fBas ⁡ X → F ∩ 𝒫 A ≠ ∅ ↔ ∃ x ∈ F x ⊆ A
19 9 18 anbi12d ⊢ F ∈ fBas ⁡ X → A ∈ 𝒫 X ∧ F ∩ 𝒫 A ≠ ∅ ↔ A ⊆ X ∧ ∃ x ∈ F x ⊆ A
20 6 19 syl5bb ⊢ F ∈ fBas ⁡ X → A ∈ y ∈ 𝒫 X | F ∩ 𝒫 y ≠ ∅ ↔ A ⊆ X ∧ ∃ x ∈ F x ⊆ A
21 2 20 bitrd ⊢ F ∈ fBas ⁡ X → A ∈ X filGen F ↔ A ⊆ X ∧ ∃ x ∈ F x ⊆ A