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

Metamath Proof Explorer

Theorem neiuni

Description: The union of the neighborhoods of a set equals the topology's underlying set. (Contributed by FL, 18-Sep-2007) (Revised by Mario Carneiro, 9-Apr-2015)

Ref Expression
Hypothesis tpnei.1 ⊢ 𝑋 = ∪ 𝐽
Assertion neiuni ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑋 = ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 tpnei.1 ⊢ 𝑋 = ∪ 𝐽
2 1 tpnei ⊢ ( 𝐽 ∈ Top → ( 𝑆 ⊆ 𝑋 ↔ 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
3 2 biimpa ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
4 elssuni ⊢ ( 𝑋 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑋 ⊆ ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
5 3 4 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑋 ⊆ ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
6 1 neii1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑥 ⊆ 𝑋 )
7 6 ex ⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑥 ⊆ 𝑋 ) )
8 7 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) → 𝑥 ⊆ 𝑋 ) )
9 8 ralrimiv ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∀ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝑥 ⊆ 𝑋 )
10 unissb ⊢ ( ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 ↔ ∀ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝑥 ⊆ 𝑋 )
11 9 10 sylibr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
12 5 11 eqssd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑋 = ∪ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )