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

Metamath Proof Explorer

Theorem isfbas2

Description: The predicate " F is a filter base." (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 28-Jul-2015)

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

Proof

Step Hyp Ref Expression
1 isfbas ⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
2 elin ⊢ ( 𝑧 ∈ ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
3 velpw ⊢ ( 𝑧 ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ↔ 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
4 3 anbi2i ⊢ ( ( 𝑧 ∈ 𝐹 ∧ 𝑧 ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
5 2 4 bitri ⊢ ( 𝑧 ∈ ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
6 5 exbii ⊢ ( ∃ 𝑧 𝑧 ∈ ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
7 n0 ⊢ ( ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
8 df-rex ⊢ ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
9 6 7 8 3bitr4i ⊢ ( ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
10 9 2ralbii ⊢ ( ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
11 10 3anbi3i ⊢ ( ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ↔ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
12 11 anbi2i ⊢ ( ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
13 1 12 bitrdi ⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )