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

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