Theorem filclus 15605

Description: The set of all cluster points of a filter.

Hypotheses

Ref	Expression
filclus.1	|- X = U.J
filclus.2	|- Y = U.F

Assertion

Ref	Expression
filclus	|- ((J e. Top /\ F e. Fil /\ X = Y) -> ((fClus` J)` F) = |^|_t e. F ((cls` J)` t))

Distinct variable groups:   t,F   t,J   t,Y

Proof of Theorem filclus

Step	Hyp	Ref	Expression
1		filclus.1	. . . . 5 |- X = U.J
2	1	sfcls 15604	. . . 4 |- (J e. Top -> (fClus` J) = {<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))})
3	2	fveq1d 4683	. . 3 |- (J e. Top -> ((fClus` J)` F) = ({<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))}` F))
4	3	3ad2ant1 897	. 2 |- ((J e. Top /\ F e. Fil /\ X = Y) -> ((fClus` J)` F) = ({<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))}` F))
5		filclus.2	. . . . . . 7 |- Y = U.F
6	5	filusb 10267	. . . . . 6 |- (F e. Fil -> Y e. F)
7		fveq2 4681	. . . . . . . . . 10 |- (t = Y -> ((cls` J)` t) = ((cls` J)` Y))
8	7	eleq2d 1964	. . . . . . . . 9 |- (t = Y -> (x e. ((cls` J)` t) <-> x e. ((cls` J)` Y)))
9	8	rcla4v 2376	. . . . . . . 8 |- (Y e. F -> (A.t e. F x e. ((cls` J)` t) -> x e. ((cls` J)` Y)))
10		visset 2295	. . . . . . . . 9 |- x e. _V
11		eliin 3260	. . . . . . . . 9 |- (x e. _V -> (x e. |^|_t e. F ((cls` J)` t) <-> A.t e. F x e. ((cls` J)` t)))
12	10, 11	ax-mp 7	. . . . . . . 8 |- (x e. |^|_t e. F ((cls` J)` t) <-> A.t e. F x e. ((cls` J)` t))
13	9, 12	syl5ib 223	. . . . . . 7 |- (Y e. F -> (x e. |^|_t e. F ((cls` J)` t) -> x e. ((cls` J)` Y)))
14	13	ssrdv 2622	. . . . . 6 |- (Y e. F -> |^|_t e. F ((cls` J)` t) C_ ((cls` J)` Y))
15		fvex 4689	. . . . . . 7 |- ((cls` J)` Y) e. _V
16	15	ssex 3455	. . . . . 6 |- (|^|_t e. F ((cls` J)` t) C_ ((cls` J)` Y) -> |^|_t e. F ((cls` J)` t) e. _V)
17	6, 14, 16	3syl 24	. . . . 5 |- (F e. Fil -> |^|_t e. F ((cls` J)` t) e. _V)
18	17	3ad2ant2 898	. . . 4 |- ((J e. Top /\ F e. Fil /\ X = Y) -> |^|_t e. F ((cls` J)` t) e. _V)
19		simp3 878	. . . . . 6 |- ((a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t)) -> b = |^|_t e. a ((cls` J)` t))
20	19	ssopab2i 3574	. . . . 5 |- {<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))} C_ {<.a, b>. | b = |^|_t e. a ((cls` J)` t)}
21		funopabeq 4456	. . . . 5 |- Fun {<.a, b>. | b = |^|_t e. a ((cls` J)` t)}
22		funss 4439	. . . . 5 |- ({<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))} C_ {<.a, b>. | b = |^|_t e. a ((cls` J)` t)} -> (Fun {<.a, b>. | b = |^|_t e. a ((cls` J)` t)} -> Fun {<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))}))
23	20, 21, 22	mp2 54	. . . 4 |- Fun {<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))}
24	18, 23	jctir 317	. . 3 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (|^|_t e. F ((cls` J)` t) e. _V /\ Fun {<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))}))
25		simp2 877	. . . . 5 |- ((J e. Top /\ F e. Fil /\ X = Y) -> F e. Fil)
26		eqcom 1886	. . . . . . 7 |- (X = Y <-> Y = X)
27	26	biimpi 168	. . . . . 6 |- (X = Y -> Y = X)
28	27	3ad2ant3 899	. . . . 5 |- ((J e. Top /\ F e. Fil /\ X = Y) -> Y = X)
29		eqidd 1885	. . . . 5 |- ((J e. Top /\ F e. Fil /\ X = Y) -> |^|_t e. F ((cls` J)` t) = |^|_t e. F ((cls` J)` t))
30	25, 28, 29	3jca 1050	. . . 4 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (F e. Fil /\ Y = X /\ |^|_t e. F ((cls` J)` t) = |^|_t e. F ((cls` J)` t)))
31		eleq1 1957	. . . . . . . 8 |- (a = F -> (a e. Fil <-> F e. Fil))
32		unieq 3185	. . . . . . . . . 10 |- (a = F -> U.a = U.F)
33	32, 5	syl6eqr 1946	. . . . . . . . 9 |- (a = F -> U.a = Y)
34	33	eqeq1d 1892	. . . . . . . 8 |- (a = F -> (U.a = X <-> Y = X))
35		iineq1 3270	. . . . . . . . 9 |- (a = F -> |^|_t e. a ((cls` J)` t) = |^|_t e. F ((cls` J)` t))
36	35	eqeq2d 1895	. . . . . . . 8 |- (a = F -> (b = |^|_t e. a ((cls` J)` t) <-> b = |^|_t e. F ((cls` J)` t)))
37	31, 34, 36	3anbi123d 1168	. . . . . . 7 |- (a = F -> ((a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t)) <-> (F e. Fil /\ Y = X /\ b = |^|_t e. F ((cls` J)` t))))
38		eqeq1 1890	. . . . . . . 8 |- (b = |^|_t e. F ((cls` J)` t) -> (b = |^|_t e. F ((cls` J)` t) <-> |^|_t e. F ((cls` J)` t) = |^|_t e. F ((cls` J)` t)))
39	38	3anbi3d 1174	. . . . . . 7 |- (b = |^|_t e. F ((cls` J)` t) -> ((F e. Fil /\ Y = X /\ b = |^|_t e. F ((cls` J)` t)) <-> (F e. Fil /\ Y = X /\ |^|_t e. F ((cls` J)` t) = |^|_t e. F ((cls` J)` t))))
40	37, 39	opelopabg 3567	. . . . . 6 |- ((F e. Fil /\ |^|_t e. F ((cls` J)` t) e. _V) -> (<.F, |^|_t e. F ((cls` J)` t)>. e. {<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))} <-> (F e. Fil /\ Y = X /\ |^|_t e. F ((cls` J)` t) = |^|_t e. F ((cls` J)` t))))
41	17, 40	mpdan 768	. . . . 5 |- (F e. Fil -> (<.F, |^|_t e. F ((cls` J)` t)>. e. {<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))} <-> (F e. Fil /\ Y = X /\ |^|_t e. F ((cls` J)` t) = |^|_t e. F ((cls` J)` t))))
42	41	3ad2ant2 898	. . . 4 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (<.F, |^|_t e. F ((cls` J)` t)>. e. {<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))} <-> (F e. Fil /\ Y = X /\ |^|_t e. F ((cls` J)` t) = |^|_t e. F ((cls` J)` t))))
43	30, 42	mpbird 213	. . 3 |- ((J e. Top /\ F e. Fil /\ X = Y) -> <.F, |^|_t e. F ((cls` J)` t)>. e. {<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))})
44		funopfvg 4711	. . 3 |- ((|^|_t e. F ((cls` J)` t) e. _V /\ Fun {<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))}) -> (<.F, |^|_t e. F ((cls` J)` t)>. e. {<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))} -> ({<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))}` F) = |^|_t e. F ((cls` J)` t)))
45	24, 43, 44	sylc 83	. 2 |- ((J e. Top /\ F e. Fil /\ X = Y) -> ({<.a, b>. | (a e. Fil /\ U.a = X /\ b = |^|_t e. a ((cls` J)` t))}` F) = |^|_t e. F ((cls` J)` t))
46	4, 45	eqtrd 1925	1 |- ((J e. Top /\ F e. Fil /\ X = Y) -> ((fClus` J)` F) = |^|_t e. F ((cls` J)` t))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292   C_ wss 2593  <.cop 3046  U.cuni 3177  |^|_ciin 3256  {copab 3395  Fun wfun 3992  ` cfv 3998  Topctop 8857  clsccl 8938  Filcfil 10264  fCluscfclus 15582

This theorem is referenced by:  isfclus 15606  fclusss 15611  fcluscomp 15621

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-13 1311  ax-14 1312  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-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iin 3258  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-fil 10265  df-fclus 15584

Copyright terms: Public domain