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

Metamath Proof Explorer

Theorem fiinbas

Description: If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion fiinbas ( ( 𝐵 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 ) → 𝐵 ∈ TopBases )

Proof

Step Hyp Ref Expression
1 ssid ⊢ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 )
2 eleq2 ⊢ ( 𝑤 = ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) )
3 sseq1 ⊢ ( 𝑤 = ( 𝑥 ∩ 𝑦 ) → ( 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
4 2 3 anbi12d ⊢ ( 𝑤 = ( 𝑥 ∩ 𝑦 ) → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
5 4 rspcev ⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 ∧ ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
6 1 5 mpanr2 ⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
7 6 ralrimiva ⊢ ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 → ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
8 7 a1i ⊢ ( 𝐵 ∈ 𝐶 → ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 → ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
9 8 ralimdv ⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
10 9 ralimdv ⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
11 isbasis2g ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
12 10 11 sylibrd ⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 → 𝐵 ∈ TopBases ) )
13 12 imp ⊢ ( ( 𝐵 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 ) → 𝐵 ∈ TopBases )