Metamath Proof Explorer

Theorem isfbas2

Description: The predicate " F is a filter base." (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion isfbas2 ⊢ B ∈ A → F ∈ fBas ⁡ B ↔ F ⊆ 𝒫 B ∧ F ≠ ∅ ∧ ∅ ∉ F ∧ ∀ x ∈ F ∀ y ∈ F ∃ z ∈ F z ⊆ x ∩ y

Proof

Step Hyp Ref Expression
1 isfbas ⊢ B ∈ A → F ∈ fBas ⁡ B ↔ F ⊆ 𝒫 B ∧ F ≠ ∅ ∧ ∅ ∉ F ∧ ∀ x ∈ F ∀ y ∈ F F ∩ 𝒫 x ∩ y ≠ ∅
2 elin ⊢ z ∈ F ∩ 𝒫 x ∩ y ↔ z ∈ F ∧ z ∈ 𝒫 x ∩ y
3 velpw ⊢ z ∈ 𝒫 x ∩ y ↔ z ⊆ x ∩ y
4 3 anbi2i ⊢ z ∈ F ∧ z ∈ 𝒫 x ∩ y ↔ z ∈ F ∧ z ⊆ x ∩ y
5 2 4 bitri ⊢ z ∈ F ∩ 𝒫 x ∩ y ↔ z ∈ F ∧ z ⊆ x ∩ y
6 5 exbii ⊢ ∃ z z ∈ F ∩ 𝒫 x ∩ y ↔ ∃ z z ∈ F ∧ z ⊆ x ∩ y
7 n0 ⊢ F ∩ 𝒫 x ∩ y ≠ ∅ ↔ ∃ z z ∈ F ∩ 𝒫 x ∩ y
8 df-rex ⊢ ∃ z ∈ F z ⊆ x ∩ y ↔ ∃ z z ∈ F ∧ z ⊆ x ∩ y
9 6 7 8 3bitr4i ⊢ F ∩ 𝒫 x ∩ y ≠ ∅ ↔ ∃ z ∈ F z ⊆ x ∩ y
10 9 2ralbii ⊢ ∀ x ∈ F ∀ y ∈ F F ∩ 𝒫 x ∩ y ≠ ∅ ↔ ∀ x ∈ F ∀ y ∈ F ∃ z ∈ F z ⊆ x ∩ y
11 10 3anbi3i ⊢ F ≠ ∅ ∧ ∅ ∉ F ∧ ∀ x ∈ F ∀ y ∈ F F ∩ 𝒫 x ∩ y ≠ ∅ ↔ F ≠ ∅ ∧ ∅ ∉ F ∧ ∀ x ∈ F ∀ y ∈ F ∃ z ∈ F z ⊆ x ∩ y
12 11 anbi2i ⊢ F ⊆ 𝒫 B ∧ F ≠ ∅ ∧ ∅ ∉ F ∧ ∀ x ∈ F ∀ y ∈ F F ∩ 𝒫 x ∩ y ≠ ∅ ↔ F ⊆ 𝒫 B ∧ F ≠ ∅ ∧ ∅ ∉ F ∧ ∀ x ∈ F ∀ y ∈ F ∃ z ∈ F z ⊆ x ∩ y
13 1 12 syl6bb ⊢ B ∈ A → F ∈ fBas ⁡ B ↔ F ⊆ 𝒫 B ∧ F ≠ ∅ ∧ ∅ ∉ F ∧ ∀ x ∈ F ∀ y ∈ F ∃ z ∈ F z ⊆ x ∩ y