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

Metamath Proof Explorer

Theorem tgtop

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

Ref Expression
Assertion tgtop ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )

Proof

Step Hyp Ref Expression
1 eltg3 ⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ ( topGen ‘ 𝐽 ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐽 ∧ 𝑥 = ∪ 𝑦 ) ) )
2 simpr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑥 = ∪ 𝑦 ) → 𝑥 = ∪ 𝑦 )
3 uniopn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ∪ 𝑦 ∈ 𝐽 )
4 3 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑥 = ∪ 𝑦 ) → ∪ 𝑦 ∈ 𝐽 )
5 2 4 eqeltrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑥 = ∪ 𝑦 ) → 𝑥 ∈ 𝐽 )
6 5 expl ⊢ ( 𝐽 ∈ Top → ( ( 𝑦 ⊆ 𝐽 ∧ 𝑥 = ∪ 𝑦 ) → 𝑥 ∈ 𝐽 ) )
7 6 exlimdv ⊢ ( 𝐽 ∈ Top → ( ∃ 𝑦 ( 𝑦 ⊆ 𝐽 ∧ 𝑥 = ∪ 𝑦 ) → 𝑥 ∈ 𝐽 ) )
8 1 7 sylbid ⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ ( topGen ‘ 𝐽 ) → 𝑥 ∈ 𝐽 ) )
9 8 ssrdv ⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) ⊆ 𝐽 )
10 bastg ⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ ( topGen ‘ 𝐽 ) )
11 9 10 eqssd ⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )