MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fbas Structured version   Visualization version   GIF version

Definition df-fbas 19564
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
StepHypRef Expression
1 cfbas 19555 . 2 class fBas
2 vw . . 3 setvar 𝑤
3 cvv 3173 . . 3 class V
4 vx . . . . . . 7 setvar 𝑥
54cv 1474 . . . . . 6 class 𝑥
6 c0 3874 . . . . . 6 class
75, 6wne 2780 . . . . 5 wff 𝑥 ≠ ∅
86, 5wnel 2781 . . . . 5 wff ∅ ∉ 𝑥
9 vy . . . . . . . . . . . 12 setvar 𝑦
109cv 1474 . . . . . . . . . . 11 class 𝑦
11 vz . . . . . . . . . . . 12 setvar 𝑧
1211cv 1474 . . . . . . . . . . 11 class 𝑧
1310, 12cin 3539 . . . . . . . . . 10 class (𝑦𝑧)
1413cpw 4108 . . . . . . . . 9 class 𝒫 (𝑦𝑧)
155, 14cin 3539 . . . . . . . 8 class (𝑥 ∩ 𝒫 (𝑦𝑧))
1615, 6wne 2780 . . . . . . 7 wff (𝑥 ∩ 𝒫 (𝑦𝑧)) ≠ ∅
1716, 11, 5wral 2896 . . . . . 6 wff 𝑧𝑥 (𝑥 ∩ 𝒫 (𝑦𝑧)) ≠ ∅
1817, 9, 5wral 2896 . . . . 5 wff 𝑦𝑥𝑧𝑥 (𝑥 ∩ 𝒫 (𝑦𝑧)) ≠ ∅
197, 8, 18w3a 1031 . . . 4 wff (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 (𝑥 ∩ 𝒫 (𝑦𝑧)) ≠ ∅)
202cv 1474 . . . . . 6 class 𝑤
2120cpw 4108 . . . . 5 class 𝒫 𝑤
2221cpw 4108 . . . 4 class 𝒫 𝒫 𝑤
2319, 4, 22crab 2900 . . 3 class {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 (𝑥 ∩ 𝒫 (𝑦𝑧)) ≠ ∅)}
242, 3, 23cmpt 4643 . 2 class (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 (𝑥 ∩ 𝒫 (𝑦𝑧)) ≠ ∅)})
251, 24wceq 1475 1 wff fBas = (𝑤 ∈ V ↦ {𝑥 ∈ 𝒫 𝒫 𝑤 ∣ (𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 (𝑥 ∩ 𝒫 (𝑦𝑧)) ≠ ∅)})
Colors of variables: wff setvar class
This definition is referenced by:  isfbas  21443
  Copyright terms: Public domain W3C validator