Theorem isfbas

Description: The predicate " F is a filter base." Note that some authors require filter bases to be closed under pairwise intersections, but that is not necessary under our definition. One advantage of this definition is that tails in a directed set form a filter base under our meaning. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Mario Carneiro, 28-Jul-2015)

	Ref	Expression
Assertion	isfbas	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-fbas	⊢ fBas = ( 𝑧 ∈ V ↦ { 𝑤 ∈ 𝒫 𝒫 𝑧 ∣ ( 𝑤 ≠ ∅ ∧ ∅ ∉ 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) } )
2		neeq1	⊢ ( 𝑤 = 𝐹 → ( 𝑤 ≠ ∅ ↔ 𝐹 ≠ ∅ ) )
3		neleq2	⊢ ( 𝑤 = 𝐹 → ( ∅ ∉ 𝑤 ↔ ∅ ∉ 𝐹 ) )
4		ineq1	⊢ ( 𝑤 = 𝐹 → ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) = ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
5	4	neeq1d	⊢ ( 𝑤 = 𝐹 → ( ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) )
6	5	raleqbi1dv	⊢ ( 𝑤 = 𝐹 → ( ∀ 𝑦 ∈ 𝑤 ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) )
7	6	raleqbi1dv	⊢ ( 𝑤 = 𝐹 → ( ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) )
8	2 3 7	3anbi123d	⊢ ( 𝑤 = 𝐹 → ( ( 𝑤 ≠ ∅ ∧ ∅ ∉ 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ↔ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) )
9	8	adantl	⊢ ( ( 𝑧 = 𝐵 ∧ 𝑤 = 𝐹 ) → ( ( 𝑤 ≠ ∅ ∧ ∅ ∉ 𝑤 ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑤 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ↔ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) )
10		pweq	⊢ ( 𝑧 = 𝐵 → 𝒫 𝑧 = 𝒫 𝐵 )
11	10	pweqd	⊢ ( 𝑧 = 𝐵 → 𝒫 𝒫 𝑧 = 𝒫 𝒫 𝐵 )
12		vpwex	⊢ 𝒫 𝑧 ∈ V
13	12	pwex	⊢ 𝒫 𝒫 𝑧 ∈ V
14	13	a1i	⊢ ( 𝑧 ∈ V → 𝒫 𝒫 𝑧 ∈ V )
15	1 9 11 14	elmptrab	⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐵 ∈ V ∧ 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) )
16		3anass	⊢ ( ( 𝐵 ∈ V ∧ 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ↔ ( 𝐵 ∈ V ∧ ( 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
17	15 16	bitri	⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐵 ∈ V ∧ ( 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
18		pwexg	⊢ ( 𝐵 ∈ 𝐴 → 𝒫 𝐵 ∈ V )
19		elpw2g	⊢ ( 𝒫 𝐵 ∈ V → ( 𝐹 ∈ 𝒫 𝒫 𝐵 ↔ 𝐹 ⊆ 𝒫 𝐵 ) )
20	18 19	syl	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 ∈ 𝒫 𝒫 𝐵 ↔ 𝐹 ⊆ 𝒫 𝐵 ) )
21	20	anbi1d	⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
22		elex	⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ∈ V )
23	22	biantrurd	⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ↔ ( 𝐵 ∈ V ∧ ( 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) ) )
24	21 23	bitr3d	⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ↔ ( 𝐵 ∈ V ∧ ( 𝐹 ∈ 𝒫 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) ) )
25	17 24	bitr4id	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )