Definition df-fbas 20575

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.)

Assertion

Ref	Expression
df-fbas	⊢ fBas = (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)})

Distinct variable group:   𝑥,𝑦,𝑧,𝑤

Detailed syntax breakdown of Definition df-fbas

Step	Hyp	Ref	Expression
1		cfbas 20566	. 2 class fBas
2		vw	. . 3 setvar 𝑤
3		cvv 3430	. . 3 class V
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1540	. . . . . 6 class 𝑥
6		c0 4261	. . . . . 6 class ∅
7	5, 6	wne 2944	. . . . 5 wff 𝑥 ≠ ∅
8	6, 5	wnel 3050	. . . . 5 wff ∅ ∉ 𝑥
9		vy	. . . . . . . . . . . 12 setvar 𝑦
10	9	cv 1540	. . . . . . . . . . 11 class 𝑦
11		vz	. . . . . . . . . . . 12 setvar 𝑧
12	11	cv 1540	. . . . . . . . . . 11 class 𝑧
13	10, 12	cin 3890	. . . . . . . . . 10 class (𝑦 ∩ 𝑧)
14	13	cpw 4538	. . . . . . . . 9 class 𝒫 (𝑦 ∩ 𝑧)
15	5, 14	cin 3890	. . . . . . . 8 class (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))
16	15, 6	wne 2944	. . . . . . 7 wff (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅
17	16, 11, 5	wral 3065	. . . . . 6 wff ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅
18	17, 9, 5	wral 3065	. . . . 5 wff ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅
19	7, 8, 18	w3a 1085	. . . 4 wff (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)
20	2	cv 1540	. . . . . 6 class 𝑤
21	20	cpw 4538	. . . . 5 class 𝒫 𝑤
22	21	cpw 4538	. . . 4 class 𝒫 𝒫 𝑤
23	19, 4, 22	crab 3069	. . 3 class {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)}
24	2, 3, 23	cmpt 5161	. 2 class (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)})
25	1, 24	wceq 1541	1 wff fBas = (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧)) ≠ ∅)})

This definition is referenced by:  isfbas  22961