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

Metamath Proof Explorer

Theorem isbasis2g

Description: Express the predicate "the set B is a basis for a topology". (Contributed by NM, 17-Jul-2006)

Ref Expression
Assertion isbasis2g ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 isbasisg ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
2 dfss3 ⊢ ( ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) 𝑧 ∈ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
3 elin ⊢ ( 𝑤 ∈ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
4 velpw ⊢ ( 𝑤 ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ↔ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) )
5 4 anbi2i ⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝑤 ∈ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
6 3 5 bitri ⊢ ( 𝑤 ∈ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
7 6 anbi2i ⊢ ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) ↔ ( 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
8 an12 ⊢ ( ( 𝑧 ∈ 𝑤 ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
9 7 8 bitri ⊢ ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
10 9 exbii ⊢ ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
11 eluni ⊢ ( 𝑧 ∈ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
12 df-rex ⊢ ( ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
13 10 11 12 3bitr4i ⊢ ( 𝑧 ∈ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
14 13 ralbii ⊢ ( ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) 𝑧 ∈ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
15 2 14 bitri ⊢ ( ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
16 15 2ralbii ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
17 1 16 bitrdi ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )