Metamath Proof Explorer

Theorem opnfbas

Description: The collection of open supersets of a nonempty set in a topology is a neighborhoods of the set, one of the motivations for the filter concept. (Contributed by Jeff Hankins, 2-Sep-2009) (Revised by Mario Carneiro, 7-Aug-2015)

Ref Expression
Hypothesis opnfbas.1 
|- X = U. J
Assertion opnfbas 
|- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> { x e. J | S C_ x } e. ( fBas ` X ) )

Proof

Step Hyp Ref Expression
1 opnfbas.1 
 |-  X = U. J
2 ssrab2 
 |-  { x e. J | S C_ x } C_ J
3 1 eqimss2i 
 |-  U. J C_ X
4 sspwuni 
 |-  ( J C_ ~P X <-> U. J C_ X )
5 3 4 mpbir 
 |-  J C_ ~P X
6 2 5 sstri 
 |-  { x e. J | S C_ x } C_ ~P X
7 6 a1i 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> { x e. J | S C_ x } C_ ~P X )
8 1 topopn 
 |-  ( J e. Top -> X e. J )
9 8 anim1i 
 |-  ( ( J e. Top /\ S C_ X ) -> ( X e. J /\ S C_ X ) )
10 9 3adant3 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( X e. J /\ S C_ X ) )
11 sseq2 
 |-  ( x = X -> ( S C_ x <-> S C_ X ) )
12 11 elrab 
 |-  ( X e. { x e. J | S C_ x } <-> ( X e. J /\ S C_ X ) )
13 10 12 sylibr 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> X e. { x e. J | S C_ x } )
14 13 ne0d 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> { x e. J | S C_ x } =/= (/) )
15 ss0 
 |-  ( S C_ (/) -> S = (/) )
16 15 necon3ai 
 |-  ( S =/= (/) -> -. S C_ (/) )
17 16 3ad2ant3 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> -. S C_ (/) )
18 17 intnand 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> -. ( (/) e. J /\ S C_ (/) ) )
19 df-nel 
 |-  ( (/) e/ { x e. J | S C_ x } <-> -. (/) e. { x e. J | S C_ x } )
20 sseq2 
 |-  ( x = (/) -> ( S C_ x <-> S C_ (/) ) )
21 20 elrab 
 |-  ( (/) e. { x e. J | S C_ x } <-> ( (/) e. J /\ S C_ (/) ) )
22 21 notbii 
 |-  ( -. (/) e. { x e. J | S C_ x } <-> -. ( (/) e. J /\ S C_ (/) ) )
23 19 22 bitr2i 
 |-  ( -. ( (/) e. J /\ S C_ (/) ) <-> (/) e/ { x e. J | S C_ x } )
24 18 23 sylib 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> (/) e/ { x e. J | S C_ x } )
25 sseq2 
 |-  ( x = r -> ( S C_ x <-> S C_ r ) )
26 25 elrab 
 |-  ( r e. { x e. J | S C_ x } <-> ( r e. J /\ S C_ r ) )
27 sseq2 
 |-  ( x = s -> ( S C_ x <-> S C_ s ) )
28 27 elrab 
 |-  ( s e. { x e. J | S C_ x } <-> ( s e. J /\ S C_ s ) )
29 26 28 anbi12i 
 |-  ( ( r e. { x e. J | S C_ x } /\ s e. { x e. J | S C_ x } ) <-> ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) )
30 simpl 
 |-  ( ( J e. Top /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> J e. Top )
31 simprll 
 |-  ( ( J e. Top /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> r e. J )
32 simprrl 
 |-  ( ( J e. Top /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> s e. J )
33 inopn 
 |-  ( ( J e. Top /\ r e. J /\ s e. J ) -> ( r i^i s ) e. J )
34 30 31 32 33 syl3anc 
 |-  ( ( J e. Top /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> ( r i^i s ) e. J )
35 ssin 
 |-  ( ( S C_ r /\ S C_ s ) <-> S C_ ( r i^i s ) )
36 35 biimpi 
 |-  ( ( S C_ r /\ S C_ s ) -> S C_ ( r i^i s ) )
37 36 ad2ant2l 
 |-  ( ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) -> S C_ ( r i^i s ) )
38 37 adantl 
 |-  ( ( J e. Top /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> S C_ ( r i^i s ) )
39 34 38 jca 
 |-  ( ( J e. Top /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> ( ( r i^i s ) e. J /\ S C_ ( r i^i s ) ) )
40 39 3ad2antl1 
 |-  ( ( ( J e. Top /\ S C_ X /\ S =/= (/) ) /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> ( ( r i^i s ) e. J /\ S C_ ( r i^i s ) ) )
41 sseq2 
 |-  ( x = ( r i^i s ) -> ( S C_ x <-> S C_ ( r i^i s ) ) )
42 41 elrab 
 |-  ( ( r i^i s ) e. { x e. J | S C_ x } <-> ( ( r i^i s ) e. J /\ S C_ ( r i^i s ) ) )
43 40 42 sylibr 
 |-  ( ( ( J e. Top /\ S C_ X /\ S =/= (/) ) /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> ( r i^i s ) e. { x e. J | S C_ x } )
44 ssid 
 |-  ( r i^i s ) C_ ( r i^i s )
45 sseq1 
 |-  ( t = ( r i^i s ) -> ( t C_ ( r i^i s ) <-> ( r i^i s ) C_ ( r i^i s ) ) )
46 45 rspcev 
 |-  ( ( ( r i^i s ) e. { x e. J | S C_ x } /\ ( r i^i s ) C_ ( r i^i s ) ) -> E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) )
47 43 44 46 sylancl 
 |-  ( ( ( J e. Top /\ S C_ X /\ S =/= (/) ) /\ ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) ) -> E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) )
48 47 ex 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( ( ( r e. J /\ S C_ r ) /\ ( s e. J /\ S C_ s ) ) -> E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) )
49 29 48 syl5bi 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( ( r e. { x e. J | S C_ x } /\ s e. { x e. J | S C_ x } ) -> E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) )
50 49 ralrimivv 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> A. r e. { x e. J | S C_ x } A. s e. { x e. J | S C_ x } E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) )
51 14 24 50 3jca 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( { x e. J | S C_ x } =/= (/) /\ (/) e/ { x e. J | S C_ x } /\ A. r e. { x e. J | S C_ x } A. s e. { x e. J | S C_ x } E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) )
52 isfbas2 
 |-  ( X e. J -> ( { x e. J | S C_ x } e. ( fBas ` X ) <-> ( { x e. J | S C_ x } C_ ~P X /\ ( { x e. J | S C_ x } =/= (/) /\ (/) e/ { x e. J | S C_ x } /\ A. r e. { x e. J | S C_ x } A. s e. { x e. J | S C_ x } E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) ) ) )
53 8 52 syl 
 |-  ( J e. Top -> ( { x e. J | S C_ x } e. ( fBas ` X ) <-> ( { x e. J | S C_ x } C_ ~P X /\ ( { x e. J | S C_ x } =/= (/) /\ (/) e/ { x e. J | S C_ x } /\ A. r e. { x e. J | S C_ x } A. s e. { x e. J | S C_ x } E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) ) ) )
54 53 3ad2ant1 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( { x e. J | S C_ x } e. ( fBas ` X ) <-> ( { x e. J | S C_ x } C_ ~P X /\ ( { x e. J | S C_ x } =/= (/) /\ (/) e/ { x e. J | S C_ x } /\ A. r e. { x e. J | S C_ x } A. s e. { x e. J | S C_ x } E. t e. { x e. J | S C_ x } t C_ ( r i^i s ) ) ) ) )
55 7 51 54 mpbir2and 
 |-  ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> { x e. J | S C_ x } e. ( fBas ` X ) )