Theorem fcluscnp 15618

Description: A function F is continuous at point A iff F respects cluster points there.

Hypotheses

Ref	Expression
fcluscnp.1	|- X = U.J
fcluscnp.2	|- Y = U.K

Assertion

Ref	Expression
fcluscnp	|- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (F e. ((J CnP K)` A) <-> A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F)))))

Distinct variable groups:   A,f   f,F   f,J   f,K   f,X   f,Y

Proof of Theorem fcluscnp

Step	Hyp	Ref	Expression
1		fcluscnp.1	. . 3 |- X = U.J
2		fcluscnp.2	. . 3 |- Y = U.K
3		eqid 1884	. . 3 |- (filGen` ({x | E.y e. g x = (F"y)} u. {Y})) = (filGen` ({x | E.y e. g x = (F"y)} u. {Y}))
4	1, 2, 3	cnpfillim 15589	. 2 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (F e. ((J CnP K)` A) <-> A.g e. Fil ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` (filGen` ({x | E.y e. g x = (F"y)} u. {Y}))))))
5		uniexg 3795	. . . . . . . . . . . 12 |- (K e. Top -> U.K e. _V)
6	5, 2	syl5eqel 1975	. . . . . . . . . . 11 |- (K e. Top -> Y e. _V)
7	6	3ad2ant2 898	. . . . . . . . . 10 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> Y e. _V)
8	7	ad2antrr 440	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (g e. Fil /\ X = U.g)) -> Y e. _V)
9		filfbas 10276	. . . . . . . . . 10 |- (g e. Fil -> g e. fBas)
10	9	ad2antrl 442	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (g e. Fil /\ X = U.g)) -> g e. fBas)
11		feq2 4552	. . . . . . . . . . 11 |- (X = U.g -> (F:X-->Y <-> F:U.g-->Y))
12		simpll3 917	. . . . . . . . . . 11 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ g e. Fil) -> F:X-->Y)
13	11, 12	syl5cbi 226	. . . . . . . . . 10 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ g e. Fil) -> (X = U.g -> F:U.g-->Y))
14	13	impr 422	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (g e. Fil /\ X = U.g)) -> F:U.g-->Y)
15		eqid 1884	. . . . . . . . . 10 |- U.g = U.g
16	15	isfilmap 10308	. . . . . . . . 9 |- ((Y e. _V /\ g e. fBas /\ F:U.g-->Y) -> ((Y FilMap g)` F) = (filGen` ({x | E.y e. g x = (F"y)} u. {Y})))
17	8, 10, 14, 16	syl111anc 1100	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (g e. Fil /\ X = U.g)) -> ((Y FilMap g)` F) = (filGen` ({x | E.y e. g x = (F"y)} u. {Y})))
18	17	fveq2d 4685	. . . . . . 7 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (g e. Fil /\ X = U.g)) -> ((fLim1` K)` ((Y FilMap g)` F)) = ((fLim1` K)` (filGen` ({x | E.y e. g x = (F"y)} u. {Y}))))
19	18	eleq2d 1964	. . . . . 6 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (g e. Fil /\ X = U.g)) -> ((F` A) e. ((fLim1` K)` ((Y FilMap g)` F)) <-> (F` A) e. ((fLim1` K)` (filGen` ({x | E.y e. g x = (F"y)} u. {Y})))))
20	19	expr 418	. . . . 5 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ g e. Fil) -> (X = U.g -> ((F` A) e. ((fLim1` K)` ((Y FilMap g)` F)) <-> (F` A) e. ((fLim1` K)` (filGen` ({x | E.y e. g x = (F"y)} u. {Y}))))))
21	20	adantrd 427	. . . 4 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ g e. Fil) -> ((X = U.g /\ A e. ((fLim1` J)` g)) -> ((F` A) e. ((fLim1` K)` ((Y FilMap g)` F)) <-> (F` A) e. ((fLim1` K)` (filGen` ({x | E.y e. g x = (F"y)} u. {Y}))))))
22	21	pm5.74d 645	. . 3 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ g e. Fil) -> (((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))) <-> ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` (filGen` ({x | E.y e. g x = (F"y)} u. {Y}))))))
23	22	ralbidva 2119	. 2 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.g e. Fil ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))) <-> A.g e. Fil ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` (filGen` ({x | E.y e. g x = (F"y)} u. {Y}))))))
24	1, 2	fcluscnplem 15617	. . 3 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.g e. Fil ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))) -> A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F)))))
25	9	ad2antrl 442	. . . . . . . . . . . 12 |- ((A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g)) -> g e. fBas)
26	25	ad2antlr 441	. . . . . . . . . . 11 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> g e. fBas)
27		simprrl 458	. . . . . . . . . . 11 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> k e. Fil)
28	11	biimpac 462	. . . . . . . . . . . . . . 15 |- ((F:X-->Y /\ X = U.g) -> F:U.g-->Y)
29	28	3ad2antl3 1040	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ X = U.g) -> F:U.g-->Y)
30	29	ad2ant2rl 447	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (g e. Fil /\ X = U.g)) -> F:U.g-->Y)
31	30	adantrl 430	. . . . . . . . . . . 12 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> F:U.g-->Y)
32	31	adantr 425	. . . . . . . . . . 11 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> F:U.g-->Y)
33		simprr 451	. . . . . . . . . . . 12 |- ((k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)) -> ((Y FilMap g)` F) C_ k)
34	33	ad2antll 443	. . . . . . . . . . 11 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> ((Y FilMap g)` F) C_ k)
35		simprl 450	. . . . . . . . . . . 12 |- ((k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)) -> Y = U.k)
36	35	ad2antll 443	. . . . . . . . . . 11 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> Y = U.k)
37		eqid 1884	. . . . . . . . . . . 12 |- U.k = U.k
38	15, 37	fmfnfm 15598	. . . . . . . . . . 11 |- (((g e. fBas /\ k e. Fil /\ F:U.g-->Y) /\ ((Y FilMap g)` F) C_ k /\ Y = U.k) -> E.j e. fBas (U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)))
39	26, 27, 32, 34, 36, 38	syl311anc 1114	. . . . . . . . . 10 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> E.j e. fBas (U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)))
40		simprr 451	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g)) -> X = U.g)
41	40	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . 21 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> X = U.g)
42		simpl1 879	. . . . . . . . . . . . . . . . . . . . . 22 |- (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) -> U.g = U.j)
43	42	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . 21 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> U.g = U.j)
44		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . 24 |- U.j = U.j
45	44	fgbas 10286	. . . . . . . . . . . . . . . . . . . . . . 23 |- (j e. fBas -> U.j = U.(filGen` j))
46	45	adantl 424	. . . . . . . . . . . . . . . . . . . . . 22 |- (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) -> U.j = U.(filGen` j))
47	46	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . 21 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> U.j = U.(filGen` j))
48	41, 43, 47	3eqtrd 1929	. . . . . . . . . . . . . . . . . . . 20 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> X = U.(filGen` j))
49		simpl2 880	. . . . . . . . . . . . . . . . . . . . . 22 |- (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) -> g C_ j)
50	49	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . 21 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> g C_ j)
51		fbssfg 10285	. . . . . . . . . . . . . . . . . . . . . . 23 |- (j e. fBas -> j C_ (filGen` j))
52	51	adantl 424	. . . . . . . . . . . . . . . . . . . . . 22 |- (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) -> j C_ (filGen` j))
53	52	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . 21 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> j C_ (filGen` j))
54	50, 53	sstrd 2627	. . . . . . . . . . . . . . . . . . . 20 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> g C_ (filGen` j))
55	48, 54	jca 310	. . . . . . . . . . . . . . . . . . 19 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> (X = U.(filGen` j) /\ g C_ (filGen` j)))
56		fgfil 10290	. . . . . . . . . . . . . . . . . . . . . 22 |- (j e. fBas -> (filGen` j) e. Fil)
57	56	adantl 424	. . . . . . . . . . . . . . . . . . . . 21 |- (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) -> (filGen` j) e. Fil)
58	57	ad2antrl 442	. . . . . . . . . . . . . . . . . . . 20 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> (filGen` j) e. Fil)
59		unieq 3185	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (h = (filGen` j) -> U.h = U.(filGen` j))
60	59	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . 23 |- (h = (filGen` j) -> (X = U.h <-> X = U.(filGen` j)))
61		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . 23 |- (h = (filGen` j) -> (g C_ h <-> g C_ (filGen` j)))
62	60, 61	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . 22 |- (h = (filGen` j) -> ((X = U.h /\ g C_ h) <-> (X = U.(filGen` j) /\ g C_ (filGen` j))))
63		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- (h = (filGen` j) -> ((fClus` J)` h) = ((fClus` J)` (filGen` j)))
64	63	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . 22 |- (h = (filGen` j) -> (A e. ((fClus` J)` h) <-> A e. ((fClus` J)` (filGen` j))))
65	62, 64	imbi12d 688	. . . . . . . . . . . . . . . . . . . . 21 |- (h = (filGen` j) -> (((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) <-> ((X = U.(filGen` j) /\ g C_ (filGen` j)) -> A e. ((fClus` J)` (filGen` j)))))
66	65	rcla4v 2376	. . . . . . . . . . . . . . . . . . . 20 |- ((filGen` j) e. Fil -> (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) -> ((X = U.(filGen` j) /\ g C_ (filGen` j)) -> A e. ((fClus` J)` (filGen` j)))))
67	58, 66	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) -> ((X = U.(filGen` j) /\ g C_ (filGen` j)) -> A e. ((fClus` J)` (filGen` j)))))
68	55, 67	mpid 58	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) -> A e. ((fClus` J)` (filGen` j))))
69		simprrr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> X = U.g)
70		simpll1 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) -> U.g = U.j)
71	70	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> U.g = U.j)
72	45	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) -> U.j = U.(filGen` j))
73	72	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> U.j = U.(filGen` j))
74	69, 71, 73	3eqtrd 1929	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> X = U.(filGen` j))
75		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> A e. ((fClus` J)` (filGen` j)))
76	74, 75	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> (X = U.(filGen` j) /\ A e. ((fClus` J)` (filGen` j))))
77		unieq 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f = (filGen` j) -> U.f = U.(filGen` j))
78	77	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f = (filGen` j) -> (X = U.f <-> X = U.(filGen` j)))
79		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f = (filGen` j) -> ((fClus` J)` f) = ((fClus` J)` (filGen` j)))
80	79	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f = (filGen` j) -> (A e. ((fClus` J)` f) <-> A e. ((fClus` J)` (filGen` j))))
81	78, 80	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f = (filGen` j) -> ((X = U.f /\ A e. ((fClus` J)` f)) <-> (X = U.(filGen` j) /\ A e. ((fClus` J)` (filGen` j)))))
82		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (f = (filGen` j) -> (Y FilMap f) = (Y FilMap (filGen` j)))
83	82	fveq1d 4683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (f = (filGen` j) -> ((Y FilMap f)` F) = ((Y FilMap (filGen` j))` F))
84	83	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (f = (filGen` j) -> ((fClus` K)` ((Y FilMap f)` F)) = ((fClus` K)` ((Y FilMap (filGen` j))` F)))
85	84	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (f = (filGen` j) -> ((F` A) e. ((fClus` K)` ((Y FilMap f)` F)) <-> (F` A) e. ((fClus` K)` ((Y FilMap (filGen` j))` F))))
86	81, 85	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f = (filGen` j) -> (((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) <-> ((X = U.(filGen` j) /\ A e. ((fClus` J)` (filGen` j))) -> (F` A) e. ((fClus` K)` ((Y FilMap (filGen` j))` F)))))
87	86	rcla4v 2376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((filGen` j) e. Fil -> (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) -> ((X = U.(filGen` j) /\ A e. ((fClus` J)` (filGen` j))) -> (F` A) e. ((fClus` K)` ((Y FilMap (filGen` j))` F)))))
88	56, 87	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (j e. fBas -> (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) -> ((X = U.(filGen` j) /\ A e. ((fClus` J)` (filGen` j))) -> (F` A) e. ((fClus` K)` ((Y FilMap (filGen` j))` F)))))
89	88	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) -> (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) -> ((X = U.(filGen` j) /\ A e. ((fClus` J)` (filGen` j))) -> (F` A) e. ((fClus` K)` ((Y FilMap (filGen` j))` F)))))
90	89	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) -> ((X = U.(filGen` j) /\ A e. ((fClus` J)` (filGen` j))) -> (F` A) e. ((fClus` K)` ((Y FilMap (filGen` j))` F)))))
91	76, 90	mpid 58	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) -> (F` A) e. ((fClus` K)` ((Y FilMap (filGen` j))` F))))
92		simpll3 917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) -> k = ((Y FilMap j)` F))
93	92	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> k = ((Y FilMap j)` F))
94	93	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> ((fClus` K)` k) = ((fClus` K)` ((Y FilMap j)` F)))
95	94	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> ((F` A) e. ((fClus` K)` k) <-> (F` A) e. ((fClus` K)` ((Y FilMap j)` F))))
96	7	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> Y e. _V)
97	96	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> Y e. _V)
98		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) -> j e. fBas)
99	98	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> j e. fBas)
100		simpl3 881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> F:X-->Y)
101	100	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> F:X-->Y)
102	69, 71	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> X = U.j)
103	102	feq2d 4557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> (F:X-->Y <-> F:U.j-->Y))
104	101, 103	mpbid 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> F:U.j-->Y)
105		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (filGen` j) = (filGen` j)
106	44, 105	fbfgfmeq 10315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((Y e. _V /\ j e. fBas /\ F:U.j-->Y) -> ((Y FilMap j)` F) = ((Y FilMap (filGen` j))` F))
107	97, 99, 104, 106	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> ((Y FilMap j)` F) = ((Y FilMap (filGen` j))` F))
108	107	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> ((fClus` K)` ((Y FilMap j)` F)) = ((fClus` K)` ((Y FilMap (filGen` j))` F)))
109	108	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> ((F` A) e. ((fClus` K)` ((Y FilMap j)` F)) <-> (F` A) e. ((fClus` K)` ((Y FilMap (filGen` j))` F))))
110	95, 109	bitr2d 588	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> ((F` A) e. ((fClus` K)` ((Y FilMap (filGen` j))` F)) <-> (F` A) e. ((fClus` K)` k)))
111	91, 110	sylibd 219	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) /\ (g e. Fil /\ X = U.g))) -> (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) -> (F` A) e. ((fClus` K)` k)))
112	111	expr 418	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> ((g e. Fil /\ X = U.g) -> (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) -> (F` A) e. ((fClus` K)` k))))
113	112	com23 36	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) -> ((g e. Fil /\ X = U.g) -> (F` A) e. ((fClus` K)` k))))
114	113	imp3a 388	. . . . . . . . . . . . . . . . . . . . 21 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ A e. ((fClus` J)` (filGen` j))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> ((A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g)) -> (F` A) e. ((fClus` K)` k)))
115	114	exp31 407	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A e. ((fClus` J)` (filGen` j)) -> ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) -> ((A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g)) -> (F` A) e. ((fClus` K)` k)))))
116	115	com24 41	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> ((A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g)) -> ((((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) -> (A e. ((fClus` J)` (filGen` j)) -> (F` A) e. ((fClus` K)` k)))))
117	116	imp31 389	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> (A e. ((fClus` J)` (filGen` j)) -> (F` A) e. ((fClus` K)` k)))
118	68, 117	syld 30	. . . . . . . . . . . . . . . . 17 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) -> (F` A) e. ((fClus` K)` k)))
119	118	expr 418	. . . . . . . . . . . . . . . 16 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ ((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas)) -> ((k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)) -> (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) -> (F` A) e. ((fClus` K)` k))))
120	119	com23 36	. . . . . . . . . . . . . . 15 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ ((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas)) -> (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) -> ((k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)) -> (F` A) e. ((fClus` K)` k))))
121	120	imp3a 388	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ ((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) /\ j e. fBas)) -> ((A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) -> (F` A) e. ((fClus` K)` k)))
122	121	exp32 408	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> ((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) -> (j e. fBas -> ((A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) -> (F` A) e. ((fClus` K)` k)))))
123	122	com24 41	. . . . . . . . . . . 12 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> ((A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k))) -> (j e. fBas -> ((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) -> (F` A) e. ((fClus` K)` k)))))
124	123	imp 377	. . . . . . . . . . 11 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> (j e. fBas -> ((U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) -> (F` A) e. ((fClus` K)` k))))
125	124	r19.23adv 2215	. . . . . . . . . 10 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> (E.j e. fBas (U.g = U.j /\ g C_ j /\ k = ((Y FilMap j)` F)) -> (F` A) e. ((fClus` K)` k)))
126	39, 125	mpd 29	. . . . . . . . 9 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) /\ (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) /\ (k e. Fil /\ (Y = U.k /\ ((Y FilMap g)` F) C_ k)))) -> (F` A) e. ((fClus` K)` k))
127	126	exp45 417	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) -> (k e. Fil -> ((Y = U.k /\ ((Y FilMap g)` F) C_ k) -> (F` A) e. ((fClus` K)` k)))))
128	127	r19.21adv 2181	. . . . . . 7 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> (A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h)) -> A.k e. Fil ((Y = U.k /\ ((Y FilMap g)` F) C_ k) -> (F` A) e. ((fClus` K)` k))))
129		simpll1 915	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> J e. Top)
130		simprrl 458	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> g e. Fil)
131		simprrr 459	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> X = U.g)
132	1, 15	flimfnfcls 15615	. . . . . . . 8 |- ((J e. Top /\ g e. Fil /\ X = U.g) -> (A e. ((fLim1` J)` g) <-> A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h))))
133	129, 130, 131, 132	syl111anc 1100	. . . . . . 7 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> (A e. ((fLim1` J)` g) <-> A.h e. Fil ((X = U.h /\ g C_ h) -> A e. ((fClus` J)` h))))
134		simpll2 916	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> K e. Top)
135	7	ad2antrr 440	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> Y e. _V)
136	9	adantr 425	. . . . . . . . . 10 |- ((g e. Fil /\ X = U.g) -> g e. fBas)
137	136	ad2antll 443	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> g e. fBas)
138		simpll3 917	. . . . . . . . . 10 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> F:X-->Y)
139	11	adantl 424	. . . . . . . . . . 11 |- ((g e. Fil /\ X = U.g) -> (F:X-->Y <-> F:U.g-->Y))
140	139	ad2antll 443	. . . . . . . . . 10 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> (F:X-->Y <-> F:U.g-->Y))
141	138, 140	mpbid 212	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> F:U.g-->Y)
142	15	fmf 10310	. . . . . . . . 9 |- ((Y e. _V /\ g e. fBas /\ F:U.g-->Y) -> ((Y FilMap g)` F) e. Fil)
143	135, 137, 141, 142	syl111anc 1100	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> ((Y FilMap g)` F) e. Fil)
144	15	fmbas 10311	. . . . . . . . . 10 |- ((Y e. _V /\ g e. fBas /\ F:U.g-->Y) -> U.((Y FilMap g)` F) = Y)
145	135, 137, 141, 144	syl111anc 1100	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> U.((Y FilMap g)` F) = Y)
146	145	eqcomd 1889	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> Y = U.((Y FilMap g)` F))
147		eqid 1884	. . . . . . . . 9 |- U.((Y FilMap g)` F) = U.((Y FilMap g)` F)
148	2, 147	flimfnfcls 15615	. . . . . . . 8 |- ((K e. Top /\ ((Y FilMap g)` F) e. Fil /\ Y = U.((Y FilMap g)` F)) -> ((F` A) e. ((fLim1` K)` ((Y FilMap g)` F)) <-> A.k e. Fil ((Y = U.k /\ ((Y FilMap g)` F) C_ k) -> (F` A) e. ((fClus` K)` k))))
149	134, 143, 146, 148	syl111anc 1100	. . . . . . 7 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> ((F` A) e. ((fLim1` K)` ((Y FilMap g)` F)) <-> A.k e. Fil ((Y = U.k /\ ((Y FilMap g)` F) C_ k) -> (F` A) e. ((fClus` K)` k))))
150	128, 133, 149	3imtr4d 602	. . . . . 6 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) /\ (g e. Fil /\ X = U.g))) -> (A e. ((fLim1` J)` g) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))))
151	150	exp45 417	. . . . 5 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) -> (g e. Fil -> (X = U.g -> (A e. ((fLim1` J)` g) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F)))))))
152	151	imp5a 400	. . . 4 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) -> (g e. Fil -> ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))))))
153	152	r19.21adv 2181	. . 3 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))) -> A.g e. Fil ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F)))))
154	24, 153	impbid 574	. 2 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.g e. Fil ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))) <-> A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F)))))
155	4, 23, 154	3bitr2d 605	1 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (F e. ((J CnP K)` A) <-> A.f e. Fil ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F)))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  {cab 1871  A.wral 2105  E.wrex 2106  _Vcvv 2292   u. cun 2591   C_ wss 2593  {csn 3044  U.cuni 3177  "cima 3989  -->wf 3994  ` cfv 3998  (class class class)co 4884  Topctop 8857   CnP ccnp 9029  fBascfbas 10257  filGencfg 10258  Filcfil 10264  fLim1cflim1 10294   FilMap cfilmap 10304  fCluscfclus 15582

This theorem is referenced by:  fcluscn 15619  fclsfcnp 15631

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-3or 859  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-reu 2111  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-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  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-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-map 5383  df-en 5427  df-fin 5430  df-top 8861  df-cld 8939  df-ntr 8940  df-cls 8941  df-nei 8989  df-cnp 9031  df-fi 10211  df-fbas 10259  df-fg 10260  df-fil 10265  df-flim1 10295  df-filmap 10306  df-fclus 15584

Copyright terms: Public domain