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 ‘ 𝐽 ) ‘ 𝑆 ) )