Theorem opnfbas 15557

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.

Hypothesis

Ref	Expression
opnfbas.1	|- X = U.J

Assertion

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

Distinct variable groups:   x,J   x,S   x,X

Proof of Theorem opnfbas

Step	Hyp	Ref	Expression
1		opnfbas.1	. . . . . . . 8 |- X = U.J
2	1	topopn 8871	. . . . . . 7 |- (J e. Top -> X e. J)
3	2	anim1i 361	. . . . . 6 |- ((J e. Top /\ S C_ X) -> (X e. J /\ S C_ X))
4	3	3adant3 896	. . . . 5 |- ((J e. Top /\ S C_ X /\ S =/= (/)) -> (X e. J /\ S C_ X))
5		sseq2 2639	. . . . . 6 |- (x = X -> (S C_ x <-> S C_ X))
6	5	elrab 2414	. . . . 5 |- (X e. {x e. J | S C_ x} <-> (X e. J /\ S C_ X))
7	4, 6	sylibr 217	. . . 4 |- ((J e. Top /\ S C_ X /\ S =/= (/)) -> X e. {x e. J | S C_ x})
8		ne0i 2881	. . . 4 |- (X e. {x e. J | S C_ x} -> {x e. J | S C_ x} =/= (/))
9	7, 8	syl 12	. . 3 |- ((J e. Top /\ S C_ X /\ S =/= (/)) -> {x e. J | S C_ x} =/= (/))
10		ss0 2902	. . . . . . 7 |- (S C_ (/) -> S = (/))
11	10	necon3ai 2043	. . . . . 6 |- (S =/= (/) -> -. S C_ (/))
12	11	3ad2ant3 899	. . . . 5 |- ((J e. Top /\ S C_ X /\ S =/= (/)) -> -. S C_ (/))
13	12	intnand 757	. . . 4 |- ((J e. Top /\ S C_ X /\ S =/= (/)) -> -. ((/) e. J /\ S C_ (/)))
14		df-nel 2020	. . . . 5 |- ((/) e/ {x e. J | S C_ x} <-> -. (/) e. {x e. J | S C_ x})
15		sseq2 2639	. . . . . . 7 |- (x = (/) -> (S C_ x <-> S C_ (/)))
16	15	elrab 2414	. . . . . 6 |- ((/) e. {x e. J | S C_ x} <-> ((/) e. J /\ S C_ (/)))
17	16	notbii 204	. . . . 5 |- (-. (/) e. {x e. J | S C_ x} <-> -. ((/) e. J /\ S C_ (/)))
18	14, 17	bitr2i 191	. . . 4 |- (-. ((/) e. J /\ S C_ (/)) <-> (/) e/ {x e. J | S C_ x})
19	13, 18	sylib 215	. . 3 |- ((J e. Top /\ S C_ X /\ S =/= (/)) -> (/) e/ {x e. J | S C_ x})
20		simpl 346	. . . . . . . . . . 11 |- ((J e. Top /\ ((r e. J /\ S C_ r) /\ (s e. J /\ S C_ s))) -> J e. Top)
21		simprll 456	. . . . . . . . . . 11 |- ((J e. Top /\ ((r e. J /\ S C_ r) /\ (s e. J /\ S C_ s))) -> r e. J)
22		simprrl 458	. . . . . . . . . . 11 |- ((J e. Top /\ ((r e. J /\ S C_ r) /\ (s e. J /\ S C_ s))) -> s e. J)
23		inopn 8869	. . . . . . . . . . 11 |- ((J e. Top /\ r e. J /\ s e. J) -> (r i^i s) e. J)
24	20, 21, 22, 23	syl111anc 1100	. . . . . . . . . 10 |- ((J e. Top /\ ((r e. J /\ S C_ r) /\ (s e. J /\ S C_ s))) -> (r i^i s) e. J)
25		ssin 2814	. . . . . . . . . . . . 13 |- ((S C_ r /\ S C_ s) <-> S C_ (r i^i s))
26	25	biimpi 168	. . . . . . . . . . . 12 |- ((S C_ r /\ S C_ s) -> S C_ (r i^i s))
27	26	ad2ant2l 444	. . . . . . . . . . 11 |- (((r e. J /\ S C_ r) /\ (s e. J /\ S C_ s)) -> S C_ (r i^i s))
28	27	adantl 424	. . . . . . . . . 10 |- ((J e. Top /\ ((r e. J /\ S C_ r) /\ (s e. J /\ S C_ s))) -> S C_ (r i^i s))
29	24, 28	jca 310	. . . . . . . . 9 |- ((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)))
30	29	3ad2antl1 1038	. . . . . . . 8 |- (((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)))
31		sseq2 2639	. . . . . . . . 9 |- (x = (r i^i s) -> (S C_ x <-> S C_ (r i^i s)))
32	31	elrab 2414	. . . . . . . 8 |- ((r i^i s) e. {x e. J | S C_ x} <-> ((r i^i s) e. J /\ S C_ (r i^i s)))
33	30, 32	sylibr 217	. . . . . . 7 |- (((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})
34		ssid 2634	. . . . . . . 8 |- (r i^i s) C_ (r i^i s)
35	34	a1i 8	. . . . . . 7 |- (((J e. Top /\ S C_ X /\ S =/= (/)) /\ ((r e. J /\ S C_ r) /\ (s e. J /\ S C_ s))) -> (r i^i s) C_ (r i^i s))
36		sseq1 2637	. . . . . . . 8 |- (t = (r i^i s) -> (t C_ (r i^i s) <-> (r i^i s) C_ (r i^i s)))
37	36	rcla4ev 2381	. . . . . . 7 |- (((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))
38	33, 35, 37	syl11anc 524	. . . . . 6 |- (((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))
39	38	ex 402	. . . . 5 |- ((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)))
40		sseq2 2639	. . . . . . 7 |- (x = r -> (S C_ x <-> S C_ r))
41	40	elrab 2414	. . . . . 6 |- (r e. {x e. J | S C_ x} <-> (r e. J /\ S C_ r))
42		sseq2 2639	. . . . . . 7 |- (x = s -> (S C_ x <-> S C_ s))
43	42	elrab 2414	. . . . . 6 |- (s e. {x e. J | S C_ x} <-> (s e. J /\ S C_ s))
44	41, 43	anbi12i 540	. . . . 5 |- ((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)))
45	39, 44	syl5ib 223	. . . 4 |- ((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)))
46	45	r19.21aivv 2183	. . 3 |- ((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))
47	9, 19, 46	3jca 1050	. 2 |- ((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)))
48		rabexg 3460	. . . 4 |- (J e. Top -> {x e. J | S C_ x} e. _V)
49		isfbas2 10263	. . . 4 |- ({x e. J | S C_ x} e. _V -> ({x e. J | S C_ x} e. fBas <-> ({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))))
50	48, 49	syl 12	. . 3 |- (J e. Top -> ({x e. J | S C_ x} e. fBas <-> ({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))))
51	50	3ad2ant1 897	. 2 |- ((J e. Top /\ S C_ X /\ S =/= (/)) -> ({x e. J | S C_ x} e. fBas <-> ({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	47, 51	mpbird 213	1 |- ((J e. Top /\ S C_ X /\ S =/= (/)) -> {x e. J | S C_ x} e. fBas)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017   e/ wnel 2018  A.wral 2105  E.wrex 2106  {crab 2108  _Vcvv 2292   i^i cin 2592   C_ wss 2593  (/)c0 2875  U.cuni 3177  Topctop 8857  fBascfbas 10257

This theorem is referenced by:  neifg 15559

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-uni 3178  df-top 8861  df-fbas 10259

Copyright terms: Public domain