Metamath Proof Explorer

Theorem opnnei

Description: A set is open iff it is a neighborhood of all of its points. (Contributed by Jeff Hankins, 15-Sep-2009)

Ref Expression
Assertion opnnei 
|- ( J e. Top -> ( S e. J <-> A. x e. S S e. ( ( nei ` J ) ` { x } ) ) )

Proof

Step Hyp Ref Expression
1 0opn 
 |-  ( J e. Top -> (/) e. J )
2 1 adantr 
 |-  ( ( J e. Top /\ S = (/) ) -> (/) e. J )
3 eleq1 
 |-  ( S = (/) -> ( S e. J <-> (/) e. J ) )
4 3 adantl 
 |-  ( ( J e. Top /\ S = (/) ) -> ( S e. J <-> (/) e. J ) )
5 2 4 mpbird 
 |-  ( ( J e. Top /\ S = (/) ) -> S e. J )
6 rzal 
 |-  ( S = (/) -> A. x e. S S e. ( ( nei ` J ) ` { x } ) )
7 6 adantl 
 |-  ( ( J e. Top /\ S = (/) ) -> A. x e. S S e. ( ( nei ` J ) ` { x } ) )
8 5 7 2thd 
 |-  ( ( J e. Top /\ S = (/) ) -> ( S e. J <-> A. x e. S S e. ( ( nei ` J ) ` { x } ) ) )
9 opnneip 
 |-  ( ( J e. Top /\ S e. J /\ x e. S ) -> S e. ( ( nei ` J ) ` { x } ) )
10 9 3expia 
 |-  ( ( J e. Top /\ S e. J ) -> ( x e. S -> S e. ( ( nei ` J ) ` { x } ) ) )
11 10 ralrimiv 
 |-  ( ( J e. Top /\ S e. J ) -> A. x e. S S e. ( ( nei ` J ) ` { x } ) )
12 11 ex 
 |-  ( J e. Top -> ( S e. J -> A. x e. S S e. ( ( nei ` J ) ` { x } ) ) )
13 12 adantr 
 |-  ( ( J e. Top /\ -. S = (/) ) -> ( S e. J -> A. x e. S S e. ( ( nei ` J ) ` { x } ) ) )
14 df-ne 
 |-  ( S =/= (/) <-> -. S = (/) )
15 r19.2z 
 |-  ( ( S =/= (/) /\ A. x e. S S e. ( ( nei ` J ) ` { x } ) ) -> E. x e. S S e. ( ( nei ` J ) ` { x } ) )
16 15 ex 
 |-  ( S =/= (/) -> ( A. x e. S S e. ( ( nei ` J ) ` { x } ) -> E. x e. S S e. ( ( nei ` J ) ` { x } ) ) )
17 14 16 sylbir 
 |-  ( -. S = (/) -> ( A. x e. S S e. ( ( nei ` J ) ` { x } ) -> E. x e. S S e. ( ( nei ` J ) ` { x } ) ) )
18 eqid 
 |-  U. J = U. J
19 18 neii1 
 |-  ( ( J e. Top /\ S e. ( ( nei ` J ) ` { x } ) ) -> S C_ U. J )
20 19 ex 
 |-  ( J e. Top -> ( S e. ( ( nei ` J ) ` { x } ) -> S C_ U. J ) )
21 20 rexlimdvw 
 |-  ( J e. Top -> ( E. x e. S S e. ( ( nei ` J ) ` { x } ) -> S C_ U. J ) )
22 17 21 sylan9r 
 |-  ( ( J e. Top /\ -. S = (/) ) -> ( A. x e. S S e. ( ( nei ` J ) ` { x } ) -> S C_ U. J ) )
23 18 ntrss2 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( ( int ` J ) ` S ) C_ S )
24 23 adantr 
 |-  ( ( ( J e. Top /\ S C_ U. J ) /\ A. x e. S { x } C_ ( ( int ` J ) ` S ) ) -> ( ( int ` J ) ` S ) C_ S )
25 vex 
 |-  x e. _V
26 25 snss 
 |-  ( x e. ( ( int ` J ) ` S ) <-> { x } C_ ( ( int ` J ) ` S ) )
27 26 ralbii 
 |-  ( A. x e. S x e. ( ( int ` J ) ` S ) <-> A. x e. S { x } C_ ( ( int ` J ) ` S ) )
28 dfss3 
 |-  ( S C_ ( ( int ` J ) ` S ) <-> A. x e. S x e. ( ( int ` J ) ` S ) )
29 28 bilanri 
 |-  ( ( ( J e. Top /\ S C_ U. J ) /\ A. x e. S x e. ( ( int ` J ) ` S ) ) -> S C_ ( ( int ` J ) ` S ) )
30 27 29 sylan2br 
 |-  ( ( ( J e. Top /\ S C_ U. J ) /\ A. x e. S { x } C_ ( ( int ` J ) ` S ) ) -> S C_ ( ( int ` J ) ` S ) )
31 24 30 eqssd 
 |-  ( ( ( J e. Top /\ S C_ U. J ) /\ A. x e. S { x } C_ ( ( int ` J ) ` S ) ) -> ( ( int ` J ) ` S ) = S )
32 31 ex 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( A. x e. S { x } C_ ( ( int ` J ) ` S ) -> ( ( int ` J ) ` S ) = S ) )
33 25 snss 
 |-  ( x e. S <-> { x } C_ S )
34 sstr2 
 |-  ( { x } C_ S -> ( S C_ U. J -> { x } C_ U. J ) )
35 34 com12 
 |-  ( S C_ U. J -> ( { x } C_ S -> { x } C_ U. J ) )
36 35 adantl 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( { x } C_ S -> { x } C_ U. J ) )
37 33 36 biimtrid 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( x e. S -> { x } C_ U. J ) )
38 37 imp 
 |-  ( ( ( J e. Top /\ S C_ U. J ) /\ x e. S ) -> { x } C_ U. J )
39 18 neiint 
 |-  ( ( J e. Top /\ { x } C_ U. J /\ S C_ U. J ) -> ( S e. ( ( nei ` J ) ` { x } ) <-> { x } C_ ( ( int ` J ) ` S ) ) )
40 39 3com23 
 |-  ( ( J e. Top /\ S C_ U. J /\ { x } C_ U. J ) -> ( S e. ( ( nei ` J ) ` { x } ) <-> { x } C_ ( ( int ` J ) ` S ) ) )
41 40 3expa 
 |-  ( ( ( J e. Top /\ S C_ U. J ) /\ { x } C_ U. J ) -> ( S e. ( ( nei ` J ) ` { x } ) <-> { x } C_ ( ( int ` J ) ` S ) ) )
42 38 41 syldan 
 |-  ( ( ( J e. Top /\ S C_ U. J ) /\ x e. S ) -> ( S e. ( ( nei ` J ) ` { x } ) <-> { x } C_ ( ( int ` J ) ` S ) ) )
43 42 ralbidva 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( A. x e. S S e. ( ( nei ` J ) ` { x } ) <-> A. x e. S { x } C_ ( ( int ` J ) ` S ) ) )
44 18 isopn3 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( S e. J <-> ( ( int ` J ) ` S ) = S ) )
45 32 43 44 3imtr4d 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( A. x e. S S e. ( ( nei ` J ) ` { x } ) -> S e. J ) )
46 45 ex 
 |-  ( J e. Top -> ( S C_ U. J -> ( A. x e. S S e. ( ( nei ` J ) ` { x } ) -> S e. J ) ) )
47 46 com23 
 |-  ( J e. Top -> ( A. x e. S S e. ( ( nei ` J ) ` { x } ) -> ( S C_ U. J -> S e. J ) ) )
48 47 adantr 
 |-  ( ( J e. Top /\ -. S = (/) ) -> ( A. x e. S S e. ( ( nei ` J ) ` { x } ) -> ( S C_ U. J -> S e. J ) ) )
49 22 48 mpdd 
 |-  ( ( J e. Top /\ -. S = (/) ) -> ( A. x e. S S e. ( ( nei ` J ) ` { x } ) -> S e. J ) )
50 13 49 impbid 
 |-  ( ( J e. Top /\ -. S = (/) ) -> ( S e. J <-> A. x e. S S e. ( ( nei ` J ) ` { x } ) ) )
51 8 50 pm2.61dan 
 |-  ( J e. Top -> ( S e. J <-> A. x e. S S e. ( ( nei ` J ) ` { x } ) ) )