Theorem isfclusf 15625

Description: The property of being a cluster point of a function.

Hypotheses

Ref	Expression
isfclusf.1	|- X = U.J
isfclusf.2	|- Y = U.L

Assertion

Ref	Expression
isfclusf	|- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> (A e. ((J fClusf L)` F) <-> (A e. X /\ A.o e. J (A e. o -> A.s e. L (o i^i (F"s)) =/= (/)))))

Distinct variable groups:   o,s,A   o,F,s   o,J,s   o,L,s   o,X,s   o,Y,s

Proof of Theorem isfclusf

Step	Hyp	Ref	Expression
1		isfclusf.1	. . . 4 |- X = U.J
2		isfclusf.2	. . . 4 |- Y = U.L
3	1, 2	sfclusf 15624	. . 3 |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> ((J fClusf L)` F) = ((fClus` J)` ((X FilMap L)` F)))
4	3	eleq2d 1964	. 2 |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> (A e. ((J fClusf L)` F) <-> A e. ((fClus` J)` ((X FilMap L)` F))))
5		simp1 876	. . 3 |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> J e. Top)
6	2	fmf 10310	. . . 4 |- ((X e. _V /\ L e. fBas /\ F:Y-->X) -> ((X FilMap L)` F) e. Fil)
7		uniexg 3795	. . . . 5 |- (J e. Top -> U.J e. _V)
8	7, 1	syl5eqel 1975	. . . 4 |- (J e. Top -> X e. _V)
9		filfbas 10276	. . . 4 |- (L e. Fil -> L e. fBas)
10		id 73	. . . 4 |- (F:Y-->X -> F:Y-->X)
11	6, 8, 9, 10	syl3an 1139	. . 3 |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> ((X FilMap L)` F) e. Fil)
12	2	fmbas 10311	. . . . 5 |- ((X e. _V /\ L e. fBas /\ F:Y-->X) -> U.((X FilMap L)` F) = X)
13	12, 8, 9, 10	syl3an 1139	. . . 4 |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> U.((X FilMap L)` F) = X)
14	13	eqcomd 1889	. . 3 |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> X = U.((X FilMap L)` F))
15		eqid 1884	. . . 4 |- U.((X FilMap L)` F) = U.((X FilMap L)` F)
16	1, 15	isfclus 15606	. . 3 |- ((J e. Top /\ ((X FilMap L)` F) e. Fil /\ X = U.((X FilMap L)` F)) -> (A e. ((fClus` J)` ((X FilMap L)` F)) <-> (A e. X /\ A.o e. J (A e. o -> A.t e. ((X FilMap L)` F)(o i^i t) =/= (/)))))
17	5, 11, 14, 16	syl111anc 1100	. 2 |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> (A e. ((fClus` J)` ((X FilMap L)` F)) <-> (A e. X /\ A.o e. J (A e. o -> A.t e. ((X FilMap L)` F)(o i^i t) =/= (/)))))
18	8, 9, 10	3anim123i 1053	. . . . . . . . . . 11 |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> (X e. _V /\ L e. fBas /\ F:Y-->X))
19	18	ad2antrr 440	. . . . . . . . . 10 |- ((((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) /\ s e. L) -> (X e. _V /\ L e. fBas /\ F:Y-->X))
20		fgid 10289	. . . . . . . . . . . . . 14 |- (L e. Fil -> (filGen` L) = L)
21	20	3ad2ant2 898	. . . . . . . . . . . . 13 |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> (filGen` L) = L)
22	21	adantr 425	. . . . . . . . . . . 12 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) -> (filGen` L) = L)
23	22	eleq2d 1964	. . . . . . . . . . 11 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) -> (s e. (filGen` L) <-> s e. L))
24	23	biimpar 461	. . . . . . . . . 10 |- ((((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) /\ s e. L) -> s e. (filGen` L))
25		eqid 1884	. . . . . . . . . . 11 |- (filGen` L) = (filGen` L)
26	2, 25	imaelfm 15591	. . . . . . . . . 10 |- (((X e. _V /\ L e. fBas /\ F:Y-->X) /\ s e. (filGen` L)) -> (F"s) e. ((X FilMap L)` F))
27	19, 24, 26	syl11anc 524	. . . . . . . . 9 |- ((((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) /\ s e. L) -> (F"s) e. ((X FilMap L)` F))
28		ineq2 2790	. . . . . . . . . . 11 |- (t = (F"s) -> (o i^i t) = (o i^i (F"s)))
29	28	neeq1d 2028	. . . . . . . . . 10 |- (t = (F"s) -> ((o i^i t) =/= (/) <-> (o i^i (F"s)) =/= (/)))
30	29	rcla4v 2376	. . . . . . . . 9 |- ((F"s) e. ((X FilMap L)` F) -> (A.t e. ((X FilMap L)` F)(o i^i t) =/= (/) -> (o i^i (F"s)) =/= (/)))
31	27, 30	syl 12	. . . . . . . 8 |- ((((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) /\ s e. L) -> (A.t e. ((X FilMap L)` F)(o i^i t) =/= (/) -> (o i^i (F"s)) =/= (/)))
32	31	r19.21adva 2182	. . . . . . 7 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) -> (A.t e. ((X FilMap L)` F)(o i^i t) =/= (/) -> A.s e. L (o i^i (F"s)) =/= (/)))
33	2	elfilmap 10312	. . . . . . . . . . . 12 |- ((X e. _V /\ L e. fBas /\ F:Y-->X) -> (t e. ((X FilMap L)` F) <-> (t C_ X /\ E.x e. L (F"x) C_ t)))
34	33, 8, 9, 10	syl3an 1139	. . . . . . . . . . 11 |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> (t e. ((X FilMap L)` F) <-> (t C_ X /\ E.x e. L (F"x) C_ t)))
35	34	adantr 425	. . . . . . . . . 10 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) -> (t e. ((X FilMap L)` F) <-> (t C_ X /\ E.x e. L (F"x) C_ t)))
36		imaeq2 4260	. . . . . . . . . . . . . . . . . . . 20 |- (s = x -> (F"s) = (F"x))
37	36	ineq2d 2796	. . . . . . . . . . . . . . . . . . 19 |- (s = x -> (o i^i (F"s)) = (o i^i (F"x)))
38	37	neeq1d 2028	. . . . . . . . . . . . . . . . . 18 |- (s = x -> ((o i^i (F"s)) =/= (/) <-> (o i^i (F"x)) =/= (/)))
39	38	rcla4v 2376	. . . . . . . . . . . . . . . . 17 |- (x e. L -> (A.s e. L (o i^i (F"s)) =/= (/) -> (o i^i (F"x)) =/= (/)))
40	39	adantr 425	. . . . . . . . . . . . . . . 16 |- ((x e. L /\ (F"x) C_ t) -> (A.s e. L (o i^i (F"s)) =/= (/) -> (o i^i (F"x)) =/= (/)))
41	40	ad2antll 443	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ ((A e. X /\ o e. J) /\ (x e. L /\ (F"x) C_ t))) -> (A.s e. L (o i^i (F"s)) =/= (/) -> (o i^i (F"x)) =/= (/)))
42		simprrr 459	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ ((A e. X /\ o e. J) /\ (x e. L /\ (F"x) C_ t))) -> (F"x) C_ t)
43		sslin 2819	. . . . . . . . . . . . . . . 16 |- ((F"x) C_ t -> (o i^i (F"x)) C_ (o i^i t))
44		ssn0 2905	. . . . . . . . . . . . . . . . 17 |- (((o i^i (F"x)) C_ (o i^i t) /\ (o i^i (F"x)) =/= (/)) -> (o i^i t) =/= (/))
45	44	ex 402	. . . . . . . . . . . . . . . 16 |- ((o i^i (F"x)) C_ (o i^i t) -> ((o i^i (F"x)) =/= (/) -> (o i^i t) =/= (/)))
46	42, 43, 45	3syl 24	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ ((A e. X /\ o e. J) /\ (x e. L /\ (F"x) C_ t))) -> ((o i^i (F"x)) =/= (/) -> (o i^i t) =/= (/)))
47	41, 46	syld 30	. . . . . . . . . . . . . 14 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ ((A e. X /\ o e. J) /\ (x e. L /\ (F"x) C_ t))) -> (A.s e. L (o i^i (F"s)) =/= (/) -> (o i^i t) =/= (/)))
48	47	expr 418	. . . . . . . . . . . . 13 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) -> ((x e. L /\ (F"x) C_ t) -> (A.s e. L (o i^i (F"s)) =/= (/) -> (o i^i t) =/= (/))))
49	48	exp3a 405	. . . . . . . . . . . 12 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) -> (x e. L -> ((F"x) C_ t -> (A.s e. L (o i^i (F"s)) =/= (/) -> (o i^i t) =/= (/)))))
50	49	r19.23adv 2215	. . . . . . . . . . 11 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) -> (E.x e. L (F"x) C_ t -> (A.s e. L (o i^i (F"s)) =/= (/) -> (o i^i t) =/= (/))))
51	50	adantld 426	. . . . . . . . . 10 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) -> ((t C_ X /\ E.x e. L (F"x) C_ t) -> (A.s e. L (o i^i (F"s)) =/= (/) -> (o i^i t) =/= (/))))
52	35, 51	sylbid 220	. . . . . . . . 9 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) -> (t e. ((X FilMap L)` F) -> (A.s e. L (o i^i (F"s)) =/= (/) -> (o i^i t) =/= (/))))
53	52	imp 377	. . . . . . . 8 |- ((((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) /\ t e. ((X FilMap L)` F)) -> (A.s e. L (o i^i (F"s)) =/= (/) -> (o i^i t) =/= (/)))
54	53	r19.21adva 2182	. . . . . . 7 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) -> (A.s e. L (o i^i (F"s)) =/= (/) -> A.t e. ((X FilMap L)` F)(o i^i t) =/= (/)))
55	32, 54	impbid 574	. . . . . 6 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) -> (A.t e. ((X FilMap L)` F)(o i^i t) =/= (/) <-> A.s e. L (o i^i (F"s)) =/= (/)))
56	55	imbi2d 674	. . . . 5 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ (A e. X /\ o e. J)) -> ((A e. o -> A.t e. ((X FilMap L)` F)(o i^i t) =/= (/)) <-> (A e. o -> A.s e. L (o i^i (F"s)) =/= (/))))
57	56	anassrs 489	. . . 4 |- ((((J e. Top /\ L e. Fil /\ F:Y-->X) /\ A e. X) /\ o e. J) -> ((A e. o -> A.t e. ((X FilMap L)` F)(o i^i t) =/= (/)) <-> (A e. o -> A.s e. L (o i^i (F"s)) =/= (/))))
58	57	ralbidva 2119	. . 3 |- (((J e. Top /\ L e. Fil /\ F:Y-->X) /\ A e. X) -> (A.o e. J (A e. o -> A.t e. ((X FilMap L)` F)(o i^i t) =/= (/)) <-> A.o e. J (A e. o -> A.s e. L (o i^i (F"s)) =/= (/))))
59	58	pm5.32da 711	. 2 |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> ((A e. X /\ A.o e. J (A e. o -> A.t e. ((X FilMap L)` F)(o i^i t) =/= (/))) <-> (A e. X /\ A.o e. J (A e. o -> A.s e. L (o i^i (F"s)) =/= (/)))))
60	4, 17, 59	3bitrd 603	1 |- ((J e. Top /\ L e. Fil /\ F:Y-->X) -> (A e. ((J fClusf L)` F) <-> (A e. X /\ A.o e. J (A e. o -> A.s e. L (o i^i (F"s)) =/= (/)))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   i^i cin 2592   C_ wss 2593  (/)c0 2875  U.cuni 3177  "cima 3989  -->wf 3994  ` cfv 3998  (class class class)co 4884  Topctop 8857  fBascfbas 10257  filGencfg 10258  Filcfil 10264   FilMap cfilmap 10304  fCluscfclus 15582   fClusf cfclusf 15583

This theorem is referenced by:  fclusfnei 15626  fclsfelbas 15627

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-nel 2020  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  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-int 3215  df-iun 3257  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-f 4010  df-fv 4014  df-opr 4886  df-oprab 4887  df-map 5383  df-top 8861  df-cld 8939  df-ntr 8940  df-cls 8941  df-fbas 10259  df-fg 10260  df-fil 10265  df-filmap 10306  df-fclus 15584  df-fclusf 15585

Copyright terms: Public domain