Metamath Proof Explorer

Definition df-fbas

Description: Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 11-Jul-2015)

Ref Expression
Assertion df-fbas ⊢ fBas = w ∈ V ⟼ x ∈ 𝒫 𝒫 w | x ≠ ∅ ∧ ∅ ∉ x ∧ ∀ y ∈ x ∀ z ∈ x x ∩ 𝒫 y ∩ z ≠ ∅

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfbas class fBas
1 vw setvar w
2 cvv class V
3 vx setvar x
4 1 cv setvar w
5 4 cpw class 𝒫 w
6 5 cpw class 𝒫 𝒫 w
7 3 cv setvar x
8 c0 class ∅
9 7 8 wne wff x ≠ ∅
10 8 7 wnel wff ∅ ∉ x
11 vy setvar y
12 vz setvar z
13 11 cv setvar y
14 12 cv setvar z
15 13 14 cin class y ∩ z
16 15 cpw class 𝒫 y ∩ z
17 7 16 cin class x ∩ 𝒫 y ∩ z
18 17 8 wne wff x ∩ 𝒫 y ∩ z ≠ ∅
19 18 12 7 wral wff ∀ z ∈ x x ∩ 𝒫 y ∩ z ≠ ∅
20 19 11 7 wral wff ∀ y ∈ x ∀ z ∈ x x ∩ 𝒫 y ∩ z ≠ ∅
21 9 10 20 w3a wff x ≠ ∅ ∧ ∅ ∉ x ∧ ∀ y ∈ x ∀ z ∈ x x ∩ 𝒫 y ∩ z ≠ ∅
22 21 3 6 crab class x ∈ 𝒫 𝒫 w | x ≠ ∅ ∧ ∅ ∉ x ∧ ∀ y ∈ x ∀ z ∈ x x ∩ 𝒫 y ∩ z ≠ ∅
23 1 2 22 cmpt class w ∈ V ⟼ x ∈ 𝒫 𝒫 w | x ≠ ∅ ∧ ∅ ∉ x ∧ ∀ y ∈ x ∀ z ∈ x x ∩ 𝒫 y ∩ z ≠ ∅
24 0 23 wceq wff fBas = w ∈ V ⟼ x ∈ 𝒫 𝒫 w | x ≠ ∅ ∧ ∅ ∉ x ∧ ∀ y ∈ x ∀ z ∈ x x ∩ 𝒫 y ∩ z ≠ ∅