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

Metamath Proof Explorer

Theorem isbasisg

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

Ref Expression
Assertion isbasisg ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 ineq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) = ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
2 1 unieqd ⊢ ( 𝑧 = 𝐵 → ∪ ( 𝑧 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) = ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
3 2 sseq2d ⊢ ( 𝑧 = 𝐵 → ( ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑧 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
4 3 raleqbi1dv ⊢ ( 𝑧 = 𝐵 → ( ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑧 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
5 4 raleqbi1dv ⊢ ( 𝑧 = 𝐵 → ( ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑧 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
6 df-bases ⊢ TopBases = { 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑧 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) }
7 5 6 elab2g ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )