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