Theorem fcluscnplem 15617

Description: Lemma for fcluscnp 15618. If a function is continuous at a point, it respects clustering there.

Hypotheses

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

Assertion

Ref	Expression
fcluscnplem	|- (((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)))))

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

Proof of Theorem fcluscnplem

Step	Hyp	Ref	Expression
1		unieq 3185	. . . . . . . . . . . . . . . . 17 |- (g = h -> U.g = U.h)
2	1	eqeq2d 1895	. . . . . . . . . . . . . . . 16 |- (g = h -> (X = U.g <-> X = U.h))
3		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (g = h -> ((fLim1` J)` g) = ((fLim1` J)` h))
4	3	eleq2d 1964	. . . . . . . . . . . . . . . 16 |- (g = h -> (A e. ((fLim1` J)` g) <-> A e. ((fLim1` J)` h)))
5	2, 4	anbi12d 690	. . . . . . . . . . . . . . 15 |- (g = h -> ((X = U.g /\ A e. ((fLim1` J)` g)) <-> (X = U.h /\ A e. ((fLim1` J)` h))))
6		opreq2 4890	. . . . . . . . . . . . . . . . . 18 |- (g = h -> (Y FilMap g) = (Y FilMap h))
7	6	fveq1d 4683	. . . . . . . . . . . . . . . . 17 |- (g = h -> ((Y FilMap g)` F) = ((Y FilMap h)` F))
8	7	fveq2d 4685	. . . . . . . . . . . . . . . 16 |- (g = h -> ((fLim1` K)` ((Y FilMap g)` F)) = ((fLim1` K)` ((Y FilMap h)` F)))
9	8	eleq2d 1964	. . . . . . . . . . . . . . 15 |- (g = h -> ((F` A) e. ((fLim1` K)` ((Y FilMap g)` F)) <-> (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))))
10	5, 9	imbi12d 688	. . . . . . . . . . . . . 14 |- (g = h -> (((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))) <-> ((X = U.h /\ A e. ((fLim1` J)` h)) -> (F` A) e. ((fLim1` K)` ((Y FilMap h)` F)))))
11	10	rcla4v 2376	. . . . . . . . . . . . 13 |- (h e. Fil -> (A.g e. Fil ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))) -> ((X = U.h /\ A e. ((fLim1` J)` h)) -> (F` A) e. ((fLim1` K)` ((Y FilMap h)` F)))))
12	11	ad2antlr 441	. . . . . . . . . . . 12 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) -> (A.g e. Fil ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))) -> ((X = U.h /\ A e. ((fLim1` J)` h)) -> (F` A) e. ((fLim1` K)` ((Y FilMap h)` F)))))
13		3simpb 873	. . . . . . . . . . . . . 14 |- ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) -> (X = U.h /\ A e. ((fLim1` J)` h)))
14	13	ad2antrl 442	. . . . . . . . . . . . 13 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) -> (X = U.h /\ A e. ((fLim1` J)` h)))
15		uniexg 3795	. . . . . . . . . . . . . . . . . . . . 21 |- (K e. Top -> U.K e. _V)
16		fcluscnp.2	. . . . . . . . . . . . . . . . . . . . 21 |- Y = U.K
17	15, 16	syl5eqel 1975	. . . . . . . . . . . . . . . . . . . 20 |- (K e. Top -> Y e. _V)
18	17	3ad2ant2 898	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> Y e. _V)
19	18	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) -> Y e. _V)
20	19	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> Y e. _V)
21		filfbas 10276	. . . . . . . . . . . . . . . . . . 19 |- (h e. Fil -> h e. fBas)
22	21	adantl 424	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) -> h e. fBas)
23	22	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> h e. fBas)
24		feq2 4552	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (X = U.h -> (F:X-->Y <-> F:U.h-->Y))
25	24	biimpac 462	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:X-->Y /\ X = U.h) -> F:U.h-->Y)
26	25	3ad2antl3 1040	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ X = U.h) -> F:U.h-->Y)
27	26	adantlr 429	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ X = U.h) -> F:U.h-->Y)
28	27	adantlr 429	. . . . . . . . . . . . . . . . . . . 20 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ X = U.h) -> F:U.h-->Y)
29	28	3ad2antr1 1041	. . . . . . . . . . . . . . . . . . 19 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ (X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h))) -> F:U.h-->Y)
30	29	adantrr 431	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) -> F:U.h-->Y)
31	30	adantr 425	. . . . . . . . . . . . . . . . 17 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> F:U.h-->Y)
32		eqid 1884	. . . . . . . . . . . . . . . . . 18 |- U.h = U.h
33	32	fmf 10310	. . . . . . . . . . . . . . . . 17 |- ((Y e. _V /\ h e. fBas /\ F:U.h-->Y) -> ((Y FilMap h)` F) e. Fil)
34	20, 23, 31, 33	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> ((Y FilMap h)` F) e. Fil)
35	32	fmbas 10311	. . . . . . . . . . . . . . . . . 18 |- ((Y e. _V /\ h e. fBas /\ F:U.h-->Y) -> U.((Y FilMap h)` F) = Y)
36	20, 23, 31, 35	syl111anc 1100	. . . . . . . . . . . . . . . . 17 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> U.((Y FilMap h)` F) = Y)
37	36	eqcomd 1889	. . . . . . . . . . . . . . . 16 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> Y = U.((Y FilMap h)` F))
38		filfbas 10276	. . . . . . . . . . . . . . . . . . . . . 22 |- (f e. Fil -> f e. fBas)
39	38	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . 21 |- (((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f)) -> f e. fBas)
40	39	ad2antlr 441	. . . . . . . . . . . . . . . . . . . 20 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> f e. fBas)
41		ffn 4562	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (F:X-->Y -> F Fn X)
42	41	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> F Fn X)
43	42	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> F Fn X)
44	43	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) -> F Fn X)
45		fneq2 4504	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (X = U.f -> (F Fn X <-> F Fn U.f))
46	45	adantl 424	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f e. Fil /\ X = U.f) -> (F Fn X <-> F Fn U.f))
47	46	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) -> (F Fn X <-> F Fn U.f))
48	44, 47	mpbid 212	. . . . . . . . . . . . . . . . . . . . 21 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) -> F Fn U.f)
49	48	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> F Fn U.f)
50		eqid 1884	. . . . . . . . . . . . . . . . . . . . 21 |- U.f = U.f
51		eqid 1884	. . . . . . . . . . . . . . . . . . . . 21 |- {x | E.y e. f x = (F"y)} = {x | E.y e. f x = (F"y)}
52	50, 51	filrn 10293	. . . . . . . . . . . . . . . . . . . 20 |- ((f e. fBas /\ F Fn U.f) -> {x | E.y e. f x = (F"y)} e. fBas)
53	40, 49, 52	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> {x | E.y e. f x = (F"y)} e. fBas)
54		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (t = (F"y) -> (t C_ Y <-> (F"y) C_ Y))
55		imassrn 4278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (F"y) C_ ran F
56	55	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (F:X-->Y -> (F"y) C_ ran F)
57		frn 4569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (F:X-->Y -> ran F C_ Y)
58	56, 57	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (F:X-->Y -> (F"y) C_ Y)
59	58	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (F"y) C_ Y)
60	59	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) -> (F"y) C_ Y)
61	60	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (F"y) C_ Y)
62	54, 61	syl5cbir 228	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (t = (F"y) -> t C_ Y))
63	62	a1d 15	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (y e. f -> (t = (F"y) -> t C_ Y)))
64	63	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (E.y e. f t = (F"y) -> t C_ Y))
65		visset 2295	. . . . . . . . . . . . . . . . . . . . . . 23 |- t e. _V
66		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = t -> (x = (F"y) <-> t = (F"y)))
67	66	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = t -> (E.y e. f x = (F"y) <-> E.y e. f t = (F"y)))
68	65, 67	elab 2403	. . . . . . . . . . . . . . . . . . . . . 22 |- (t e. {x | E.y e. f x = (F"y)} <-> E.y e. f t = (F"y))
69	64, 68	syl5ib 223	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (t e. {x | E.y e. f x = (F"y)} -> t C_ Y))
70	69	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . 20 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> A.t e. {x | E.y e. f x = (F"y)}t C_ Y)
71		unissb 3208	. . . . . . . . . . . . . . . . . . . 20 |- (U.{x | E.y e. f x = (F"y)} C_ Y <-> A.t e. {x | E.y e. f x = (F"y)}t C_ Y)
72	70, 71	sylibr 217	. . . . . . . . . . . . . . . . . . 19 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> U.{x | E.y e. f x = (F"y)} C_ Y)
73		eqid 1884	. . . . . . . . . . . . . . . . . . . 20 |- U.{x | E.y e. f x = (F"y)} = U.{x | E.y e. f x = (F"y)}
74	73	extbas1 10291	. . . . . . . . . . . . . . . . . . 19 |- (({x | E.y e. f x = (F"y)} e. fBas /\ U.{x | E.y e. f x = (F"y)} C_ Y) -> ({x | E.y e. f x = (F"y)} u. {Y}) e. fBas)
75	53, 72, 74	syl11anc 524	. . . . . . . . . . . . . . . . . 18 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> ({x | E.y e. f x = (F"y)} u. {Y}) e. fBas)
76	42	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) -> F Fn X)
77	76	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> F Fn X)
78		fneq2 4504	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (X = U.h -> (F Fn X <-> F Fn U.h))
79	78	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) -> (F Fn X <-> F Fn U.h))
80	79	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 |- (((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f)) -> (F Fn X <-> F Fn U.h))
81	80	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (F Fn X <-> F Fn U.h))
82	77, 81	mpbid 212	. . . . . . . . . . . . . . . . . . . 20 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> F Fn U.h)
83		eqid 1884	. . . . . . . . . . . . . . . . . . . . 21 |- {x | E.y e. h x = (F"y)} = {x | E.y e. h x = (F"y)}
84	32, 83	filrn 10293	. . . . . . . . . . . . . . . . . . . 20 |- ((h e. fBas /\ F Fn U.h) -> {x | E.y e. h x = (F"y)} e. fBas)
85	23, 82, 84	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> {x | E.y e. h x = (F"y)} e. fBas)
86	54, 58	syl5cbir 228	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (F:X-->Y -> (t = (F"y) -> t C_ Y))
87	86	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (t = (F"y) -> t C_ Y))
88	87	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) -> (t = (F"y) -> t C_ Y))
89	88	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (t = (F"y) -> t C_ Y))
90	89	a1d 15	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (y e. h -> (t = (F"y) -> t C_ Y)))
91	90	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (E.y e. h t = (F"y) -> t C_ Y))
92	66	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = t -> (E.y e. h x = (F"y) <-> E.y e. h t = (F"y)))
93	65, 92	elab 2403	. . . . . . . . . . . . . . . . . . . . . 22 |- (t e. {x | E.y e. h x = (F"y)} <-> E.y e. h t = (F"y))
94	91, 93	syl5ib 223	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (t e. {x | E.y e. h x = (F"y)} -> t C_ Y))
95	94	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . 20 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> A.t e. {x | E.y e. h x = (F"y)}t C_ Y)
96		unissb 3208	. . . . . . . . . . . . . . . . . . . 20 |- (U.{x | E.y e. h x = (F"y)} C_ Y <-> A.t e. {x | E.y e. h x = (F"y)}t C_ Y)
97	95, 96	sylibr 217	. . . . . . . . . . . . . . . . . . 19 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> U.{x | E.y e. h x = (F"y)} C_ Y)
98		eqid 1884	. . . . . . . . . . . . . . . . . . . 20 |- U.{x | E.y e. h x = (F"y)} = U.{x | E.y e. h x = (F"y)}
99	98	extbas1 10291	. . . . . . . . . . . . . . . . . . 19 |- (({x | E.y e. h x = (F"y)} e. fBas /\ U.{x | E.y e. h x = (F"y)} C_ Y) -> ({x | E.y e. h x = (F"y)} u. {Y}) e. fBas)
100	85, 97, 99	syl11anc 524	. . . . . . . . . . . . . . . . . 18 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> ({x | E.y e. h x = (F"y)} u. {Y}) e. fBas)
101		ssrexv 2673	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f C_ h -> (E.y e. f x = (F"y) -> E.y e. h x = (F"y)))
102	101	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . . 22 |- ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) -> (E.y e. f x = (F"y) -> E.y e. h x = (F"y)))
103	102	adantr 425	. . . . . . . . . . . . . . . . . . . . 21 |- (((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f)) -> (E.y e. f x = (F"y) -> E.y e. h x = (F"y)))
104	103	ad2antlr 441	. . . . . . . . . . . . . . . . . . . 20 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (E.y e. f x = (F"y) -> E.y e. h x = (F"y)))
105	104	19.21aiv 1664	. . . . . . . . . . . . . . . . . . 19 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> A.x(E.y e. f x = (F"y) -> E.y e. h x = (F"y)))
106		ss2ab 2675	. . . . . . . . . . . . . . . . . . . 20 |- ({x | E.y e. f x = (F"y)} C_ {x | E.y e. h x = (F"y)} <-> A.x(E.y e. f x = (F"y) -> E.y e. h x = (F"y)))
107		unss1 2773	. . . . . . . . . . . . . . . . . . . 20 |- ({x | E.y e. f x = (F"y)} C_ {x | E.y e. h x = (F"y)} -> ({x | E.y e. f x = (F"y)} u. {Y}) C_ ({x | E.y e. h x = (F"y)} u. {Y}))
108	106, 107	sylbir 218	. . . . . . . . . . . . . . . . . . 19 |- (A.x(E.y e. f x = (F"y) -> E.y e. h x = (F"y)) -> ({x | E.y e. f x = (F"y)} u. {Y}) C_ ({x | E.y e. h x = (F"y)} u. {Y}))
109	105, 108	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> ({x | E.y e. f x = (F"y)} u. {Y}) C_ ({x | E.y e. h x = (F"y)} u. {Y}))
110		fgss 10287	. . . . . . . . . . . . . . . . . 18 |- ((({x | E.y e. f x = (F"y)} u. {Y}) e. fBas /\ ({x | E.y e. h x = (F"y)} u. {Y}) e. fBas /\ ({x | E.y e. f x = (F"y)} u. {Y}) C_ ({x | E.y e. h x = (F"y)} u. {Y})) -> (filGen` ({x | E.y e. f x = (F"y)} u. {Y})) C_ (filGen` ({x | E.y e. h x = (F"y)} u. {Y})))
111	75, 100, 109, 110	syl111anc 1100	. . . . . . . . . . . . . . . . 17 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (filGen` ({x | E.y e. f x = (F"y)} u. {Y})) C_ (filGen` ({x | E.y e. h x = (F"y)} u. {Y})))
112		feq2 4552	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (X = U.f -> (F:X-->Y <-> F:U.f-->Y))
113	112	biimpac 462	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:X-->Y /\ X = U.f) -> F:U.f-->Y)
114	113	3ad2antl3 1040	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ X = U.f) -> F:U.f-->Y)
115	114	adantlr 429	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ X = U.f) -> F:U.f-->Y)
116	115	ad2ant2rl 447	. . . . . . . . . . . . . . . . . . . 20 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ X = U.f)) -> F:U.f-->Y)
117	116	adantrrl 438	. . . . . . . . . . . . . . . . . . 19 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) -> F:U.f-->Y)
118	117	adantr 425	. . . . . . . . . . . . . . . . . 18 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> F:U.f-->Y)
119	50	isfilmap 10308	. . . . . . . . . . . . . . . . . 18 |- ((Y e. _V /\ f e. fBas /\ F:U.f-->Y) -> ((Y FilMap f)` F) = (filGen` ({x | E.y e. f x = (F"y)} u. {Y})))
120	20, 40, 118, 119	syl111anc 1100	. . . . . . . . . . . . . . . . 17 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> ((Y FilMap f)` F) = (filGen` ({x | E.y e. f x = (F"y)} u. {Y})))
121	32	isfilmap 10308	. . . . . . . . . . . . . . . . . 18 |- ((Y e. _V /\ h e. fBas /\ F:U.h-->Y) -> ((Y FilMap h)` F) = (filGen` ({x | E.y e. h x = (F"y)} u. {Y})))
122	20, 23, 31, 121	syl111anc 1100	. . . . . . . . . . . . . . . . 17 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> ((Y FilMap h)` F) = (filGen` ({x | E.y e. h x = (F"y)} u. {Y})))
123	111, 120, 122	3sstr4d 2660	. . . . . . . . . . . . . . . 16 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> ((Y FilMap f)` F) C_ ((Y FilMap h)` F))
124		simpr 350	. . . . . . . . . . . . . . . 16 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> (F` A) e. ((fLim1` K)` ((Y FilMap h)` F)))
125		unieq 3185	. . . . . . . . . . . . . . . . . . 19 |- (k = ((Y FilMap h)` F) -> U.k = U.((Y FilMap h)` F))
126	125	eqeq2d 1895	. . . . . . . . . . . . . . . . . 18 |- (k = ((Y FilMap h)` F) -> (Y = U.k <-> Y = U.((Y FilMap h)` F)))
127		sseq2 2639	. . . . . . . . . . . . . . . . . 18 |- (k = ((Y FilMap h)` F) -> (((Y FilMap f)` F) C_ k <-> ((Y FilMap f)` F) C_ ((Y FilMap h)` F)))
128		fveq2 4681	. . . . . . . . . . . . . . . . . . 19 |- (k = ((Y FilMap h)` F) -> ((fLim1` K)` k) = ((fLim1` K)` ((Y FilMap h)` F)))
129	128	eleq2d 1964	. . . . . . . . . . . . . . . . . 18 |- (k = ((Y FilMap h)` F) -> ((F` A) e. ((fLim1` K)` k) <-> (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))))
130	126, 127, 129	3anbi123d 1168	. . . . . . . . . . . . . . . . 17 |- (k = ((Y FilMap h)` F) -> ((Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k)) <-> (Y = U.((Y FilMap h)` F) /\ ((Y FilMap f)` F) C_ ((Y FilMap h)` F) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F)))))
131	130	rcla4ev 2381	. . . . . . . . . . . . . . . 16 |- ((((Y FilMap h)` F) e. Fil /\ (Y = U.((Y FilMap h)` F) /\ ((Y FilMap f)` F) C_ ((Y FilMap h)` F) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F)))) -> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k)))
132	34, 37, 123, 124, 131	syl13anc 1102	. . . . . . . . . . . . . . 15 |- ((((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) /\ (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k)))
133	132	ex 402	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) -> ((F` A) e. ((fLim1` K)` ((Y FilMap h)` F)) -> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k))))
134	133	imim2d 28	. . . . . . . . . . . . 13 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) -> (((X = U.h /\ A e. ((fLim1` J)` h)) -> (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> ((X = U.h /\ A e. ((fLim1` J)` h)) -> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k)))))
135	14, 134	mpid 58	. . . . . . . . . . . 12 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) -> (((X = U.h /\ A e. ((fLim1` J)` h)) -> (F` A) e. ((fLim1` K)` ((Y FilMap h)` F))) -> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k))))
136	12, 135	syld 30	. . . . . . . . . . 11 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ h e. Fil) /\ ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) /\ (f e. Fil /\ X = U.f))) -> (A.g e. Fil ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))) -> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k))))
137	136	exp43 415	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (h e. Fil -> ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) -> ((f e. Fil /\ X = U.f) -> (A.g e. Fil ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))) -> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k)))))))
138	137	com45 46	. . . . . . . . 9 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (h e. Fil -> ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) -> (A.g e. Fil ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))) -> ((f e. Fil /\ X = U.f) -> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k)))))))
139	138	com35 47	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (h e. Fil -> ((f e. Fil /\ X = U.f) -> (A.g e. Fil ((X = U.g /\ A e. ((fLim1` J)` g)) -> (F` A) e. ((fLim1` K)` ((Y FilMap g)` F))) -> ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) -> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k)))))))
140	139	com24 41	. . . . . . 7 |- (((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))) -> ((f e. Fil /\ X = U.f) -> (h e. Fil -> ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) -> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k)))))))
141	140	imp32 390	. . . . . 6 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> (h e. Fil -> ((X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) -> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k)))))
142	141	r19.23adv 2215	. . . . 5 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> (E.h e. Fil (X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h)) -> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k))))
143		simpll1 915	. . . . . 6 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> J e. Top)
144		simprrl 458	. . . . . 6 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> f e. Fil)
145		simprrr 459	. . . . . 6 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> X = U.f)
146		fcluscnp.1	. . . . . . 7 |- X = U.J
147	146, 50	fclsfnflim 15614	. . . . . 6 |- ((J e. Top /\ f e. Fil /\ X = U.f) -> (A e. ((fClus` J)` f) <-> E.h e. Fil (X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h))))
148	143, 144, 145, 147	syl111anc 1100	. . . . 5 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> (A e. ((fClus` J)` f) <-> E.h e. Fil (X = U.h /\ f C_ h /\ A e. ((fLim1` J)` h))))
149		simpll2 916	. . . . . 6 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> K e. Top)
150	18	ad2antrr 440	. . . . . . 7 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> Y e. _V)
151	38	adantr 425	. . . . . . . 8 |- ((f e. Fil /\ X = U.f) -> f e. fBas)
152	151	ad2antll 443	. . . . . . 7 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> f e. fBas)
153		simpll3 917	. . . . . . . 8 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> F:X-->Y)
154	112	adantl 424	. . . . . . . . 9 |- ((f e. Fil /\ X = U.f) -> (F:X-->Y <-> F:U.f-->Y))
155	154	ad2antll 443	. . . . . . . 8 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> (F:X-->Y <-> F:U.f-->Y))
156	153, 155	mpbid 212	. . . . . . 7 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> F:U.f-->Y)
157	50	fmf 10310	. . . . . . 7 |- ((Y e. _V /\ f e. fBas /\ F:U.f-->Y) -> ((Y FilMap f)` F) e. Fil)
158	150, 152, 156, 157	syl111anc 1100	. . . . . 6 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> ((Y FilMap f)` F) e. Fil)
159	50	fmbas 10311	. . . . . . . 8 |- ((Y e. _V /\ f e. fBas /\ F:U.f-->Y) -> U.((Y FilMap f)` F) = Y)
160	150, 152, 156, 159	syl111anc 1100	. . . . . . 7 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> U.((Y FilMap f)` F) = Y)
161	160	eqcomd 1889	. . . . . 6 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> Y = U.((Y FilMap f)` F))
162		eqid 1884	. . . . . . 7 |- U.((Y FilMap f)` F) = U.((Y FilMap f)` F)
163	16, 162	fclsfnflim 15614	. . . . . 6 |- ((K e. Top /\ ((Y FilMap f)` F) e. Fil /\ Y = U.((Y FilMap f)` F)) -> ((F` A) e. ((fClus` K)` ((Y FilMap f)` F)) <-> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k))))
164	149, 158, 161, 163	syl111anc 1100	. . . . 5 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> ((F` A) e. ((fClus` K)` ((Y FilMap f)` F)) <-> E.k e. Fil (Y = U.k /\ ((Y FilMap f)` F) C_ k /\ (F` A) e. ((fLim1` K)` k))))
165	142, 148, 164	3imtr4d 602	. . . 4 |- ((((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))) /\ (f e. Fil /\ X = U.f))) -> (A e. ((fClus` J)` f) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))))
166	165	exp45 417	. . 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))) -> (f e. Fil -> (X = U.f -> (A e. ((fClus` J)` f) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F)))))))
167	166	imp5a 400	. 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))) -> (f e. Fil -> ((X = U.f /\ A e. ((fClus` J)` f)) -> (F` A) e. ((fClus` K)` ((Y FilMap f)` F))))))
168	167	r19.21adv 2181	1 |- (((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)))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = 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  ran crn 3987  "cima 3989   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  Topctop 8857  fBascfbas 10257  filGencfg 10258  Filcfil 10264  fLim1cflim1 10294   FilMap cfilmap 10304  fCluscfclus 15582

This theorem is referenced by:  fcluscnp 15618

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-fi 10211  df-fbas 10259  df-fg 10260  df-fil 10265  df-flim1 10295  df-filmap 10306  df-fclus 15584

Copyright terms: Public domain