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

Metamath Proof Explorer

Theorem topbas

Description: A topology is its own basis. (Contributed by NM, 17-Jul-2006)

Ref Expression
Assertion topbas ( 𝐽 ∈ Top → 𝐽 ∈ TopBases )

Proof

Step Hyp Ref Expression
1 inopn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 )
2 1 3expb ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 )
3 simpr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) )
4 ssid ⊢ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 )
5 3 4 jctir ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
6 eleq2 ⊢ ( 𝑤 = ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) )
7 sseq1 ⊢ ( 𝑤 = ( 𝑥 ∩ 𝑦 ) → ( 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
8 6 7 anbi12d ⊢ ( 𝑤 = ( 𝑥 ∩ 𝑦 ) → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
9 8 rspcev ⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 ∧ ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) → ∃ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
10 2 5 9 syl2an2r ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
11 10 exp31 ⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) → ∃ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
12 11 ralrimdv ⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) → ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
13 12 ralrimivv ⊢ ( 𝐽 ∈ Top → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
14 isbasis2g ⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
15 13 14 mpbird ⊢ ( 𝐽 ∈ Top → 𝐽 ∈ TopBases )