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 ) )