This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑤 ∈ V ↦ { 𝑥 ∈ 𝒫 𝒫 𝑤 ∣ ( 𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfbas ⊢ fBas
1 vw ⊢ 𝑤
2 cvv ⊢ V
3 vx ⊢ 𝑥
4 1 cv ⊢ 𝑤
5 4 cpw ⊢ 𝒫 𝑤
6 5 cpw ⊢ 𝒫 𝒫 𝑤
7 3 cv ⊢ 𝑥
8 c0 ⊢ ∅
9 7 8 wne ⊢ 𝑥 ≠ ∅
10 8 7 wnel ⊢ ∅ ∉ 𝑥
11 vy ⊢ 𝑦
12 vz ⊢ 𝑧
13 11 cv ⊢ 𝑦
14 12 cv ⊢ 𝑧
15 13 14 cin ⊢ ( 𝑦 ∩ 𝑧 )
16 15 cpw ⊢ 𝒫 ( 𝑦 ∩ 𝑧 )
17 7 16 cin ⊢ ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) )
18 17 8 wne ⊢ ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅
19 18 12 7 wral ⊢ ∀ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅
20 19 11 7 wral ⊢ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅
21 9 10 20 w3a ⊢ ( 𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ )
22 21 3 6 crab ⊢ { 𝑥 ∈ 𝒫 𝒫 𝑤 ∣ ( 𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) }
23 1 2 22 cmpt ⊢ ( 𝑤 ∈ V ↦ { 𝑥 ∈ 𝒫 𝒫 𝑤 ∣ ( 𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) } )
24 0 23 wceq ⊢ fBas = ( 𝑤 ∈ V ↦ { 𝑥 ∈ 𝒫 𝒫 𝑤 ∣ ( 𝑥 ≠ ∅ ∧ ∅ ∉ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) ≠ ∅ ) } )