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

Metamath Proof Explorer

Theorem isbasis3g

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

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

Proof

Step Hyp Ref Expression
1 isbasis2g ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
2 elssuni ⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ⊆ ∪ 𝐵 )
3 2 rgen ⊢ ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵
4 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 )
5 4 biimpi ⊢ ( 𝑥 ∈ ∪ 𝐵 → ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 )
6 5 rgen ⊢ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦
7 3 6 pm3.2i ⊢ ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 )
8 7 biantrur ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ( ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
9 df-3an ⊢ ( ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ↔ ( ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
10 8 9 bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
11 1 10 bitrdi ⊢ ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )