Metamath Proof Explorer


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 ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥𝐹𝑦𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥𝑦 ) ) ≠ ∅ ) ) ) )