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 
|- X = U. J
Assertion neiuni 
|- ( ( J e. Top /\ S C_ X ) -> X = U. ( ( nei ` J ) ` S ) )

Proof

Step Hyp Ref Expression
1 tpnei.1 
 |-  X = U. J
2 1 tpnei 
 |-  ( J e. Top -> ( S C_ X <-> X e. ( ( nei ` J ) ` S ) ) )
3 2 biimpa 
 |-  ( ( J e. Top /\ S C_ X ) -> X e. ( ( nei ` J ) ` S ) )
4 elssuni 
 |-  ( X e. ( ( nei ` J ) ` S ) -> X C_ U. ( ( nei ` J ) ` S ) )
5 3 4 syl 
 |-  ( ( J e. Top /\ S C_ X ) -> X C_ U. ( ( nei ` J ) ` S ) )
6 1 neii1 
 |-  ( ( J e. Top /\ x e. ( ( nei ` J ) ` S ) ) -> x C_ X )
7 6 ex 
 |-  ( J e. Top -> ( x e. ( ( nei ` J ) ` S ) -> x C_ X ) )
8 7 adantr 
 |-  ( ( J e. Top /\ S C_ X ) -> ( x e. ( ( nei ` J ) ` S ) -> x C_ X ) )
9 8 ralrimiv 
 |-  ( ( J e. Top /\ S C_ X ) -> A. x e. ( ( nei ` J ) ` S ) x C_ X )
10 unissb 
 |-  ( U. ( ( nei ` J ) ` S ) C_ X <-> A. x e. ( ( nei ` J ) ` S ) x C_ X )
11 9 10 sylibr 
 |-  ( ( J e. Top /\ S C_ X ) -> U. ( ( nei ` J ) ` S ) C_ X )
12 5 11 eqssd 
 |-  ( ( J e. Top /\ S C_ X ) -> X = U. ( ( nei ` J ) ` S ) )