Theorem cnpfillim 15589

Description: Continuity of a function at a point in terms of filter limits. (Contributed by Jeff Hankins, 7-Sep-2009.)

Hypotheses

Ref	Expression
cnfillim.1	|- X = U.J
cnfillim.2	|- Y = U.K
cnfillim.3	|- L = (filGen` ({y | E.z e. f y = (F"z)} u. {Y}))

Assertion

Ref	Expression
cnpfillim	|- (((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. ((fLim1` J)` f)) -> (F` A) e. ((fLim1` K)` L))))

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

Proof of Theorem cnpfillim

Step	Hyp	Ref	Expression
1		cnfillim.1	. . 3 |- X = U.J
2		cnfillim.2	. . 3 |- Y = U.K
3	1, 2	cnpnei 9043	. 2 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (F e. ((J CnP K)` A) <-> A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})))
4		simp2 877	. . . . . . . . . . 11 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> K e. Top)
5	4	adantr 425	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> K e. Top)
6	5	ad2antrr 440	. . . . . . . . 9 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> K e. Top)
7		filfbas 10276	. . . . . . . . . . . . . 14 |- (f e. Fil -> f e. fBas)
8	7	adantr 425	. . . . . . . . . . . . 13 |- ((f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f))) -> f e. fBas)
9	8	ad2antlr 441	. . . . . . . . . . . 12 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> f e. fBas)
10		ffn 4562	. . . . . . . . . . . . . . . . . 18 |- (F:X-->Y -> F Fn X)
11	10	adantr 425	. . . . . . . . . . . . . . . . 17 |- ((F:X-->Y /\ X = U.f) -> F Fn X)
12		fneq2 4504	. . . . . . . . . . . . . . . . . 18 |- (X = U.f -> (F Fn X <-> F Fn U.f))
13	12	adantl 424	. . . . . . . . . . . . . . . . 17 |- ((F:X-->Y /\ X = U.f) -> (F Fn X <-> F Fn U.f))
14	11, 13	mpbid 212	. . . . . . . . . . . . . . . 16 |- ((F:X-->Y /\ X = U.f) -> F Fn U.f)
15	14	3ad2antl3 1040	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ X = U.f) -> F Fn U.f)
16	15	adantrr 431	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (X = U.f /\ A e. ((fLim1` J)` f))) -> F Fn U.f)
17	16	ad2ant2rl 447	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) -> F Fn U.f)
18	17	adantr 425	. . . . . . . . . . . 12 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> F Fn U.f)
19		eqid 1884	. . . . . . . . . . . . 13 |- U.f = U.f
20		eqid 1884	. . . . . . . . . . . . 13 |- {y | E.z e. f y = (F"z)} = {y | E.z e. f y = (F"z)}
21	19, 20	filrn 10293	. . . . . . . . . . . 12 |- ((f e. fBas /\ F Fn U.f) -> {y | E.z e. f y = (F"z)} e. fBas)
22	9, 18, 21	syl11anc 524	. . . . . . . . . . 11 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> {y | E.z e. f y = (F"z)} e. fBas)
23		funimaexg 4495	. . . . . . . . . . . . . . . . . 18 |- ((Fun F /\ z e. f) -> (F"z) e. _V)
24		ffun 4565	. . . . . . . . . . . . . . . . . 18 |- (F:X-->Y -> Fun F)
25	23, 24	sylan 497	. . . . . . . . . . . . . . . . 17 |- ((F:X-->Y /\ z e. f) -> (F"z) e. _V)
26	25	r19.21aiva 2176	. . . . . . . . . . . . . . . 16 |- (F:X-->Y -> A.z e. f (F"z) e. _V)
27		dfiun2g 3283	. . . . . . . . . . . . . . . 16 |- (A.z e. f (F"z) e. _V -> U_z e. f (F"z) = U.{y | E.z e. f y = (F"z)})
28	26, 27	syl 12	. . . . . . . . . . . . . . 15 |- (F:X-->Y -> U_z e. f (F"z) = U.{y | E.z e. f y = (F"z)})
29		imassrn 4278	. . . . . . . . . . . . . . . . . . . 20 |- (F"z) C_ ran F
30	29	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (F:X-->Y -> (F"z) C_ ran F)
31		frn 4569	. . . . . . . . . . . . . . . . . . 19 |- (F:X-->Y -> ran F C_ Y)
32	30, 31	sstrd 2627	. . . . . . . . . . . . . . . . . 18 |- (F:X-->Y -> (F"z) C_ Y)
33	32	a1d 15	. . . . . . . . . . . . . . . . 17 |- (F:X-->Y -> (z e. f -> (F"z) C_ Y))
34	33	r19.21aiv 2175	. . . . . . . . . . . . . . . 16 |- (F:X-->Y -> A.z e. f (F"z) C_ Y)
35		iunss 3291	. . . . . . . . . . . . . . . 16 |- (U_z e. f (F"z) C_ Y <-> A.z e. f (F"z) C_ Y)
36	34, 35	sylibr 217	. . . . . . . . . . . . . . 15 |- (F:X-->Y -> U_z e. f (F"z) C_ Y)
37	28, 36	eqsstr3d 2652	. . . . . . . . . . . . . 14 |- (F:X-->Y -> U.{y | E.z e. f y = (F"z)} C_ Y)
38	37	3ad2ant3 899	. . . . . . . . . . . . 13 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> U.{y | E.z e. f y = (F"z)} C_ Y)
39	38	adantr 425	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> U.{y | E.z e. f y = (F"z)} C_ Y)
40	39	ad2antrr 440	. . . . . . . . . . 11 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> U.{y | E.z e. f y = (F"z)} C_ Y)
41		eqid 1884	. . . . . . . . . . . 12 |- U.{y | E.z e. f y = (F"z)} = U.{y | E.z e. f y = (F"z)}
42	41	extbas1 10291	. . . . . . . . . . 11 |- (({y | E.z e. f y = (F"z)} e. fBas /\ U.{y | E.z e. f y = (F"z)} C_ Y) -> ({y | E.z e. f y = (F"z)} u. {Y}) e. fBas)
43	22, 40, 42	syl11anc 524	. . . . . . . . . 10 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> ({y | E.z e. f y = (F"z)} u. {Y}) e. fBas)
44		fgfil 10290	. . . . . . . . . . 11 |- (({y | E.z e. f y = (F"z)} u. {Y}) e. fBas -> (filGen` ({y | E.z e. f y = (F"z)} u. {Y})) e. Fil)
45		cnfillim.3	. . . . . . . . . . 11 |- L = (filGen` ({y | E.z e. f y = (F"z)} u. {Y}))
46	44, 45	syl5eqel 1975	. . . . . . . . . 10 |- (({y | E.z e. f y = (F"z)} u. {Y}) e. fBas -> L e. Fil)
47	43, 46	syl 12	. . . . . . . . 9 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> L e. Fil)
48		uniexg 3795	. . . . . . . . . . . . . . 15 |- (K e. Top -> U.K e. _V)
49	48, 2	syl5eqel 1975	. . . . . . . . . . . . . 14 |- (K e. Top -> Y e. _V)
50	49	3ad2ant2 898	. . . . . . . . . . . . 13 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> Y e. _V)
51	50	adantr 425	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> Y e. _V)
52	51	ad2antrr 440	. . . . . . . . . . 11 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> Y e. _V)
53	41	extbas2 10292	. . . . . . . . . . 11 |- ((U.{y | E.z e. f y = (F"z)} C_ Y /\ Y e. _V) -> U.({y | E.z e. f y = (F"z)} u. {Y}) = Y)
54	40, 52, 53	syl11anc 524	. . . . . . . . . 10 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> U.({y | E.z e. f y = (F"z)} u. {Y}) = Y)
55		eqid 1884	. . . . . . . . . . . . 13 |- U.({y | E.z e. f y = (F"z)} u. {Y}) = U.({y | E.z e. f y = (F"z)} u. {Y})
56	55	fgbas 10286	. . . . . . . . . . . 12 |- (({y | E.z e. f y = (F"z)} u. {Y}) e. fBas -> U.({y | E.z e. f y = (F"z)} u. {Y}) = U.(filGen` ({y | E.z e. f y = (F"z)} u. {Y})))
57	45	unieqi 3187	. . . . . . . . . . . 12 |- U.L = U.(filGen` ({y | E.z e. f y = (F"z)} u. {Y}))
58	56, 57	syl6eqr 1946	. . . . . . . . . . 11 |- (({y | E.z e. f y = (F"z)} u. {Y}) e. fBas -> U.({y | E.z e. f y = (F"z)} u. {Y}) = U.L)
59	43, 58	syl 12	. . . . . . . . . 10 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> U.({y | E.z e. f y = (F"z)} u. {Y}) = U.L)
60	54, 59	eqtr3d 1927	. . . . . . . . 9 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> Y = U.L)
61		eqid 1884	. . . . . . . . . 10 |- U.L = U.L
62	2, 61	isfillim 10298	. . . . . . . . 9 |- ((K e. Top /\ L e. Fil /\ Y = U.L) -> ((F` A) e. ((fLim1` K)` L) <-> ((F` A) e. Y /\ ((nei` K)` {(F` A)}) C_ L)))
63	6, 47, 60, 62	syl111anc 1100	. . . . . . . 8 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> ((F` A) e. ((fLim1` K)` L) <-> ((F` A) e. Y /\ ((nei` K)` {(F` A)}) C_ L)))
64		ffvelrn 4787	. . . . . . . . . 10 |- ((F:X-->Y /\ A e. X) -> (F` A) e. Y)
65	64	3ad2antl3 1040	. . . . . . . . 9 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (F` A) e. Y)
66	65	ad2antrr 440	. . . . . . . 8 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> (F` A) e. Y)
67		imaeq2 4260	. . . . . . . . . . . . . . . 16 |- (x = w -> (`'F"x) = (`'F"w))
68	67	eleq1d 1963	. . . . . . . . . . . . . . 15 |- (x = w -> ((`'F"x) e. ((nei` J)` {A}) <-> (`'F"w) e. ((nei` J)` {A})))
69	68	rcla4v 2376	. . . . . . . . . . . . . 14 |- (w e. ((nei` K)` {(F` A)}) -> (A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}) -> (`'F"w) e. ((nei` J)` {A})))
70	69	adantl 424	. . . . . . . . . . . . 13 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ w e. ((nei` K)` {(F` A)})) -> (A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}) -> (`'F"w) e. ((nei` J)` {A})))
71		simp1 876	. . . . . . . . . . . . . . . 16 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> J e. Top)
72	71	adantr 425	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> J e. Top)
73	72	ad2antrr 440	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ w e. ((nei` K)` {(F` A)})) -> J e. Top)
74		simplrl 454	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ w e. ((nei` K)` {(F` A)})) -> f e. Fil)
75		simprl 450	. . . . . . . . . . . . . . 15 |- ((f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f))) -> X = U.f)
76	75	ad2antlr 441	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ w e. ((nei` K)` {(F` A)})) -> X = U.f)
77		simprr 451	. . . . . . . . . . . . . . 15 |- ((f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f))) -> A e. ((fLim1` J)` f))
78	77	ad2antlr 441	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ w e. ((nei` K)` {(F` A)})) -> A e. ((fLim1` J)` f))
79	1, 19	flimnei 10301	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ A e. ((fLim1` J)` f) /\ (`'F"w) e. ((nei` J)` {A})) -> (`'F"w) e. f)
80	79	3expia 1069	. . . . . . . . . . . . . 14 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ A e. ((fLim1` J)` f)) -> ((`'F"w) e. ((nei` J)` {A}) -> (`'F"w) e. f))
81	73, 74, 76, 78, 80	syl31anc 1103	. . . . . . . . . . . . 13 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ w e. ((nei` K)` {(F` A)})) -> ((`'F"w) e. ((nei` J)` {A}) -> (`'F"w) e. f))
82	8	ad2antlr 441	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> f e. fBas)
83	17	adantr 425	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> F Fn U.f)
84	82, 83, 21	syl11anc 524	. . . . . . . . . . . . . . . . 17 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> {y | E.z e. f y = (F"z)} e. fBas)
85	39	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> U.{y | E.z e. f y = (F"z)} C_ Y)
86	84, 85, 42	syl11anc 524	. . . . . . . . . . . . . . . 16 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> ({y | E.z e. f y = (F"z)} u. {Y}) e. fBas)
87	55	elfg 10284	. . . . . . . . . . . . . . . . 17 |- (({y | E.z e. f y = (F"z)} u. {Y}) e. fBas -> (w e. (filGen` ({y | E.z e. f y = (F"z)} u. {Y})) <-> (w C_ U.({y | E.z e. f y = (F"z)} u. {Y}) /\ E.a e. ({y | E.z e. f y = (F"z)} u. {Y})a C_ w)))
88	45	eleq2i 1961	. . . . . . . . . . . . . . . . 17 |- (w e. L <-> w e. (filGen` ({y | E.z e. f y = (F"z)} u. {Y})))
89	87, 88	syl5bb 591	. . . . . . . . . . . . . . . 16 |- (({y | E.z e. f y = (F"z)} u. {Y}) e. fBas -> (w e. L <-> (w C_ U.({y | E.z e. f y = (F"z)} u. {Y}) /\ E.a e. ({y | E.z e. f y = (F"z)} u. {Y})a C_ w)))
90	86, 89	syl 12	. . . . . . . . . . . . . . 15 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> (w e. L <-> (w C_ U.({y | E.z e. f y = (F"z)} u. {Y}) /\ E.a e. ({y | E.z e. f y = (F"z)} u. {Y})a C_ w)))
91	2	neii1 8997	. . . . . . . . . . . . . . . . . . 19 |- ((K e. Top /\ w e. ((nei` K)` {(F` A)})) -> w C_ Y)
92	91	3ad2antl2 1039	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ w e. ((nei` K)` {(F` A)})) -> w C_ Y)
93	92	adantlr 429	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ w e. ((nei` K)` {(F` A)})) -> w C_ Y)
94	93	ad2ant2r 445	. . . . . . . . . . . . . . . 16 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> w C_ Y)
95	51	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> Y e. _V)
96	85, 95, 53	syl11anc 524	. . . . . . . . . . . . . . . 16 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> U.({y | E.z e. f y = (F"z)} u. {Y}) = Y)
97	94, 96	sseqtr4d 2654	. . . . . . . . . . . . . . 15 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> w C_ U.({y | E.z e. f y = (F"z)} u. {Y}))
98		ssun1 2767	. . . . . . . . . . . . . . . . . 18 |- {y | E.z e. f y = (F"z)} C_ ({y | E.z e. f y = (F"z)} u. {Y})
99	98	a1i 8	. . . . . . . . . . . . . . . . 17 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> {y | E.z e. f y = (F"z)} C_ ({y | E.z e. f y = (F"z)} u. {Y}))
100		eqid 1884	. . . . . . . . . . . . . . . . . . . 20 |- (F"(`'F"w)) = (F"(`'F"w))
101		imaeq2 4260	. . . . . . . . . . . . . . . . . . . . . 22 |- (z = (`'F"w) -> (F"z) = (F"(`'F"w)))
102	101	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . 21 |- (z = (`'F"w) -> ((F"(`'F"w)) = (F"z) <-> (F"(`'F"w)) = (F"(`'F"w))))
103	102	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . 20 |- (((`'F"w) e. f /\ (F"(`'F"w)) = (F"(`'F"w))) -> E.z e. f (F"(`'F"w)) = (F"z))
104	100, 103	mpan2 760	. . . . . . . . . . . . . . . . . . 19 |- ((`'F"w) e. f -> E.z e. f (F"(`'F"w)) = (F"z))
105	104	ad2antll 443	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> E.z e. f (F"(`'F"w)) = (F"z))
106		funimaexg 4495	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((Fun F /\ (`'F"w) e. f) -> (F"(`'F"w)) e. _V)
107	106, 24	sylan 497	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F:X-->Y /\ (`'F"w) e. f) -> (F"(`'F"w)) e. _V)
108	107	3ad2antl3 1040	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ (`'F"w) e. f) -> (F"(`'F"w)) e. _V)
109	108	adantlr 429	. . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (`'F"w) e. f) -> (F"(`'F"w)) e. _V)
110	109	ad2ant2rl 447	. . . . . . . . . . . . . . . . . . 19 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> (F"(`'F"w)) e. _V)
111		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (F"(`'F"w)) -> (y = (F"z) <-> (F"(`'F"w)) = (F"z)))
112	111	rexbidv 2124	. . . . . . . . . . . . . . . . . . . 20 |- (y = (F"(`'F"w)) -> (E.z e. f y = (F"z) <-> E.z e. f (F"(`'F"w)) = (F"z)))
113	112	elabg 2405	. . . . . . . . . . . . . . . . . . 19 |- ((F"(`'F"w)) e. _V -> ((F"(`'F"w)) e. {y | E.z e. f y = (F"z)} <-> E.z e. f (F"(`'F"w)) = (F"z)))
114	110, 113	syl 12	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> ((F"(`'F"w)) e. {y | E.z e. f y = (F"z)} <-> E.z e. f (F"(`'F"w)) = (F"z)))
115	105, 114	mpbird 213	. . . . . . . . . . . . . . . . 17 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> (F"(`'F"w)) e. {y | E.z e. f y = (F"z)})
116	99, 115	sseldd 2620	. . . . . . . . . . . . . . . 16 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> (F"(`'F"w)) e. ({y | E.z e. f y = (F"z)} u. {Y}))
117		ssid 2634	. . . . . . . . . . . . . . . . . . . . 21 |- (`'F"w) C_ (`'F"w)
118		funimass2 4492	. . . . . . . . . . . . . . . . . . . . 21 |- ((Fun F /\ (`'F"w) C_ (`'F"w)) -> (F"(`'F"w)) C_ w)
119	117, 118	mpan2 760	. . . . . . . . . . . . . . . . . . . 20 |- (Fun F -> (F"(`'F"w)) C_ w)
120	24, 119	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (F:X-->Y -> (F"(`'F"w)) C_ w)
121	120	3ad2ant3 899	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (F"(`'F"w)) C_ w)
122	121	adantr 425	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (F"(`'F"w)) C_ w)
123	122	ad2antrr 440	. . . . . . . . . . . . . . . 16 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> (F"(`'F"w)) C_ w)
124		sseq1 2637	. . . . . . . . . . . . . . . . 17 |- (a = (F"(`'F"w)) -> (a C_ w <-> (F"(`'F"w)) C_ w))
125	124	rcla4ev 2381	. . . . . . . . . . . . . . . 16 |- (((F"(`'F"w)) e. ({y | E.z e. f y = (F"z)} u. {Y}) /\ (F"(`'F"w)) C_ w) -> E.a e. ({y | E.z e. f y = (F"z)} u. {Y})a C_ w)
126	116, 123, 125	syl11anc 524	. . . . . . . . . . . . . . 15 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> E.a e. ({y | E.z e. f y = (F"z)} u. {Y})a C_ w)
127	90, 97, 126	mpbir2and 802	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ (w e. ((nei` K)` {(F` A)}) /\ (`'F"w) e. f)) -> w e. L)
128	127	expr 418	. . . . . . . . . . . . 13 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ w e. ((nei` K)` {(F` A)})) -> ((`'F"w) e. f -> w e. L))
129	70, 81, 128	3syld 31	. . . . . . . . . . . 12 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ w e. ((nei` K)` {(F` A)})) -> (A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}) -> w e. L))
130	129	ex 402	. . . . . . . . . . 11 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) -> (w e. ((nei` K)` {(F` A)}) -> (A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}) -> w e. L)))
131	130	com23 36	. . . . . . . . . 10 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) -> (A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}) -> (w e. ((nei` K)` {(F` A)}) -> w e. L)))
132	131	imp 377	. . . . . . . . 9 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> (w e. ((nei` K)` {(F` A)}) -> w e. L))
133	132	ssrdv 2622	. . . . . . . 8 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> ((nei` K)` {(F` A)}) C_ L)
134	63, 66, 133	mpbir2and 802	. . . . . . 7 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (f e. Fil /\ (X = U.f /\ A e. ((fLim1` J)` f)))) /\ A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})) -> (F` A) e. ((fLim1` K)` L))
135	134	exp42 414	. . . . . 6 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (f e. Fil -> ((X = U.f /\ A e. ((fLim1` J)` f)) -> (A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}) -> (F` A) e. ((fLim1` K)` L)))))
136	135	com23 36	. . . . 5 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> ((X = U.f /\ A e. ((fLim1` J)` f)) -> (f e. Fil -> (A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}) -> (F` A) e. ((fLim1` K)` L)))))
137	136	com24 41	. . . 4 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}) -> (f e. Fil -> ((X = U.f /\ A e. ((fLim1` J)` f)) -> (F` A) e. ((fLim1` K)` L)))))
138	137	r19.21adv 2181	. . 3 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}) -> A.f e. Fil ((X = U.f /\ A e. ((fLim1` J)` f)) -> (F` A) e. ((fLim1` K)` L))))
139		simpl 346	. . . . . . 7 |- ((J e. Top /\ A e. X) -> J e. Top)
140		snssi 3129	. . . . . . . 8 |- (A e. X -> {A} C_ X)
141	140	adantl 424	. . . . . . 7 |- ((J e. Top /\ A e. X) -> {A} C_ X)
142		snnzg 3118	. . . . . . . 8 |- (A e. X -> {A} =/= (/))
143	142	adantl 424	. . . . . . 7 |- ((J e. Top /\ A e. X) -> {A} =/= (/))
144	1	neifil 10302	. . . . . . 7 |- ((J e. Top /\ {A} C_ X /\ {A} =/= (/)) -> ((nei` J)` {A}) e. Fil)
145	139, 141, 143, 144	syl111anc 1100	. . . . . 6 |- ((J e. Top /\ A e. X) -> ((nei` J)` {A}) e. Fil)
146	145	3ad2antl1 1038	. . . . 5 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> ((nei` J)` {A}) e. Fil)
147		unieq 3185	. . . . . . . . 9 |- (f = ((nei` J)` {A}) -> U.f = U.((nei` J)` {A}))
148	147	eqeq2d 1895	. . . . . . . 8 |- (f = ((nei` J)` {A}) -> (X = U.f <-> X = U.((nei` J)` {A})))
149		fveq2 4681	. . . . . . . . 9 |- (f = ((nei` J)` {A}) -> ((fLim1` J)` f) = ((fLim1` J)` ((nei` J)` {A})))
150	149	eleq2d 1964	. . . . . . . 8 |- (f = ((nei` J)` {A}) -> (A e. ((fLim1` J)` f) <-> A e. ((fLim1` J)` ((nei` J)` {A}))))
151	148, 150	anbi12d 690	. . . . . . 7 |- (f = ((nei` J)` {A}) -> ((X = U.f /\ A e. ((fLim1` J)` f)) <-> (X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A})))))
152		rexeq 2267	. . . . . . . . . . . . 13 |- (f = ((nei` J)` {A}) -> (E.z e. f y = (F"z) <-> E.z e. ((nei` J)` {A})y = (F"z)))
153	152	abbidv 2008	. . . . . . . . . . . 12 |- (f = ((nei` J)` {A}) -> {y | E.z e. f y = (F"z)} = {y | E.z e. ((nei` J)` {A})y = (F"z)})
154	153	uneq1d 2754	. . . . . . . . . . 11 |- (f = ((nei` J)` {A}) -> ({y | E.z e. f y = (F"z)} u. {Y}) = ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))
155	154	fveq2d 4685	. . . . . . . . . 10 |- (f = ((nei` J)` {A}) -> (filGen` ({y | E.z e. f y = (F"z)} u. {Y})) = (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))
156	155, 45	syl5eq 1940	. . . . . . . . 9 |- (f = ((nei` J)` {A}) -> L = (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))
157	156	fveq2d 4685	. . . . . . . 8 |- (f = ((nei` J)` {A}) -> ((fLim1` K)` L) = ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))))
158	157	eleq2d 1964	. . . . . . 7 |- (f = ((nei` J)` {A}) -> ((F` A) e. ((fLim1` K)` L) <-> (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))))
159	151, 158	imbi12d 688	. . . . . 6 |- (f = ((nei` J)` {A}) -> (((X = U.f /\ A e. ((fLim1` J)` f)) -> (F` A) e. ((fLim1` K)` L)) <-> ((X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A}))) -> (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))))))
160	159	rcla4v 2376	. . . . 5 |- (((nei` J)` {A}) e. Fil -> (A.f e. Fil ((X = U.f /\ A e. ((fLim1` J)` f)) -> (F` A) e. ((fLim1` K)` L)) -> ((X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A}))) -> (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))))))
161	146, 160	syl 12	. . . 4 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.f e. Fil ((X = U.f /\ A e. ((fLim1` J)` f)) -> (F` A) e. ((fLim1` K)` L)) -> ((X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A}))) -> (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))))))
162	1	unnei 9011	. . . . . . . . 9 |- ((J e. Top /\ {A} C_ X) -> U.((nei` J)` {A}) = X)
163	162, 140	sylan2 500	. . . . . . . 8 |- ((J e. Top /\ A e. X) -> U.((nei` J)` {A}) = X)
164	163	eqcomd 1889	. . . . . . 7 |- ((J e. Top /\ A e. X) -> X = U.((nei` J)` {A}))
165	1	neiplim 15586	. . . . . . 7 |- ((J e. Top /\ A e. X) -> A e. ((fLim1` J)` ((nei` J)` {A})))
166	164, 165	jca 310	. . . . . 6 |- ((J e. Top /\ A e. X) -> (X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A}))))
167	166	3ad2antl1 1038	. . . . 5 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A}))))
168		pm2.27 76	. . . . . . 7 |- ((X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A}))) -> (((X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A}))) -> (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))))
169		simpll2 916	. . . . . . . . . . . 12 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> K e. Top)
170		filfbas 10276	. . . . . . . . . . . . . . . . . 18 |- (((nei` J)` {A}) e. Fil -> ((nei` J)` {A}) e. fBas)
171	145, 170	syl 12	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ A e. X) -> ((nei` J)` {A}) e. fBas)
172	171	3ad2antl1 1038	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> ((nei` J)` {A}) e. fBas)
173	172	adantr 425	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> ((nei` J)` {A}) e. fBas)
174	10	3ad2ant3 899	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> F Fn X)
175	174	adantr 425	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> F Fn X)
176	163	fneq2d 4506	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ A e. X) -> (F Fn U.((nei` J)` {A}) <-> F Fn X))
177	176	3ad2antl1 1038	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (F Fn U.((nei` J)` {A}) <-> F Fn X))
178	175, 177	mpbird 213	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> F Fn U.((nei` J)` {A}))
179	178	adantr 425	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> F Fn U.((nei` J)` {A}))
180		eqid 1884	. . . . . . . . . . . . . . . 16 |- U.((nei` J)` {A}) = U.((nei` J)` {A})
181		eqid 1884	. . . . . . . . . . . . . . . 16 |- {y | E.z e. ((nei` J)` {A})y = (F"z)} = {y | E.z e. ((nei` J)` {A})y = (F"z)}
182	180, 181	filrn 10293	. . . . . . . . . . . . . . 15 |- ((((nei` J)` {A}) e. fBas /\ F Fn U.((nei` J)` {A})) -> {y | E.z e. ((nei` J)` {A})y = (F"z)} e. fBas)
183	173, 179, 182	syl11anc 524	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> {y | E.z e. ((nei` J)` {A})y = (F"z)} e. fBas)
184		funimaexg 4495	. . . . . . . . . . . . . . . . . . . 20 |- ((Fun F /\ z e. ((nei` J)` {A})) -> (F"z) e. _V)
185	184, 24	sylan 497	. . . . . . . . . . . . . . . . . . 19 |- ((F:X-->Y /\ z e. ((nei` J)` {A})) -> (F"z) e. _V)
186	185	r19.21aiva 2176	. . . . . . . . . . . . . . . . . 18 |- (F:X-->Y -> A.z e. ((nei` J)` {A})(F"z) e. _V)
187		dfiun2g 3283	. . . . . . . . . . . . . . . . . 18 |- (A.z e. ((nei` J)` {A})(F"z) e. _V -> U_z e. ((nei` J)` {A})(F"z) = U.{y | E.z e. ((nei` J)` {A})y = (F"z)})
188	186, 187	syl 12	. . . . . . . . . . . . . . . . 17 |- (F:X-->Y -> U_z e. ((nei` J)` {A})(F"z) = U.{y | E.z e. ((nei` J)` {A})y = (F"z)})
189	32	a1d 15	. . . . . . . . . . . . . . . . . . 19 |- (F:X-->Y -> (z e. ((nei` J)` {A}) -> (F"z) C_ Y))
190	189	r19.21aiv 2175	. . . . . . . . . . . . . . . . . 18 |- (F:X-->Y -> A.z e. ((nei` J)` {A})(F"z) C_ Y)
191		iunss 3291	. . . . . . . . . . . . . . . . . 18 |- (U_z e. ((nei` J)` {A})(F"z) C_ Y <-> A.z e. ((nei` J)` {A})(F"z) C_ Y)
192	190, 191	sylibr 217	. . . . . . . . . . . . . . . . 17 |- (F:X-->Y -> U_z e. ((nei` J)` {A})(F"z) C_ Y)
193	188, 192	eqsstr3d 2652	. . . . . . . . . . . . . . . 16 |- (F:X-->Y -> U.{y | E.z e. ((nei` J)` {A})y = (F"z)} C_ Y)
194	193	3ad2ant3 899	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> U.{y | E.z e. ((nei` J)` {A})y = (F"z)} C_ Y)
195	194	ad2antrr 440	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> U.{y | E.z e. ((nei` J)` {A})y = (F"z)} C_ Y)
196		eqid 1884	. . . . . . . . . . . . . . 15 |- U.{y | E.z e. ((nei` J)` {A})y = (F"z)} = U.{y | E.z e. ((nei` J)` {A})y = (F"z)}
197	196	extbas1 10291	. . . . . . . . . . . . . 14 |- (({y | E.z e. ((nei` J)` {A})y = (F"z)} e. fBas /\ U.{y | E.z e. ((nei` J)` {A})y = (F"z)} C_ Y) -> ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) e. fBas)
198	183, 195, 197	syl11anc 524	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) e. fBas)
199		fgfil 10290	. . . . . . . . . . . . 13 |- (({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) e. fBas -> (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})) e. Fil)
200	198, 199	syl 12	. . . . . . . . . . . 12 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})) e. Fil)
201	194	adantr 425	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> U.{y | E.z e. ((nei` J)` {A})y = (F"z)} C_ Y)
202	196	extbas2 10292	. . . . . . . . . . . . . . 15 |- ((U.{y | E.z e. ((nei` J)` {A})y = (F"z)} C_ Y /\ Y e. _V) -> U.({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) = Y)
203	201, 51, 202	syl11anc 524	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> U.({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) = Y)
204	203	adantr 425	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> U.({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) = Y)
205		eqid 1884	. . . . . . . . . . . . . . 15 |- U.({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) = U.({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})
206	205	fgbas 10286	. . . . . . . . . . . . . 14 |- (({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) e. fBas -> U.({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) = U.(filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))
207	198, 206	syl 12	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> U.({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) = U.(filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))
208	204, 207	eqtr3d 1927	. . . . . . . . . . . 12 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> Y = U.(filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))
209	169, 200, 208	3jca 1050	. . . . . . . . . . 11 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (K e. Top /\ (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})) e. Fil /\ Y = U.(filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))))
210		eqid 1884	. . . . . . . . . . . . 13 |- U.(filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})) = U.(filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))
211	2, 210	flimnei 10301	. . . . . . . . . . . 12 |- (((K e. Top /\ (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})) e. Fil /\ Y = U.(filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))) /\ x e. ((nei` K)` {(F` A)})) -> x e. (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))
212	211	3expia 1069	. . . . . . . . . . 11 |- (((K e. Top /\ (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})) e. Fil /\ Y = U.(filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (x e. ((nei` K)` {(F` A)}) -> x e. (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))))
213	209, 212	sylancom 531	. . . . . . . . . 10 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (x e. ((nei` K)` {(F` A)}) -> x e. (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))))
214	205	elfg 10284	. . . . . . . . . . . . . 14 |- (({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) e. fBas -> (x e. (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})) <-> (x C_ U.({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) /\ E.w e. ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})w C_ x)))
215	198, 214	syl 12	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (x e. (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})) <-> (x C_ U.({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) /\ E.w e. ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})w C_ x)))
216	204	sseq2d 2645	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (x C_ U.({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) <-> x C_ Y))
217	216	anbi1d 679	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> ((x C_ U.({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) /\ E.w e. ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})w C_ x) <-> (x C_ Y /\ E.w e. ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})w C_ x)))
218	215, 217	bitrd 587	. . . . . . . . . . . 12 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (x e. (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})) <-> (x C_ Y /\ E.w e. ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})w C_ x)))
219	24	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> Fun F)
220	219	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> Fun F)
221	1	neii1 8997	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((J e. Top /\ z e. ((nei` J)` {A})) -> z C_ X)
222	221	3ad2antl1 1038	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ z e. ((nei` J)` {A})) -> z C_ X)
223	222	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> z C_ X)
224		fdm 4567	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (F:X-->Y -> dom F = X)
225	224	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> dom F = X)
226	225	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> dom F = X)
227	226	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> (z C_ dom F <-> z C_ X))
228	223, 227	mpbird 213	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> z C_ dom F)
229		funimass3 4779	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((Fun F /\ z C_ dom F) -> ((F"z) C_ w <-> z C_ (`'F"w)))
230	220, 228, 229	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> ((F"z) C_ w <-> z C_ (`'F"w)))
231		fimacnv 4783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (F:X-->Y -> (`'F"Y) = X)
232	231	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((J e. Top /\ K e. Top /\ F:X-->Y) -> (`'F"Y) = X)
233	232	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> (`'F"Y) = X)
234	233	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> ((`'F"x) C_ (`'F"Y) <-> (`'F"x) C_ X))
235	1	ssnei2 9006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((J e. Top /\ z e. ((nei` J)` {A})) /\ (z C_ (`'F"x) /\ (`'F"x) C_ X)) -> (`'F"x) e. ((nei` J)` {A}))
236	235	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((J e. Top /\ z e. ((nei` J)` {A})) -> ((z C_ (`'F"x) /\ (`'F"x) C_ X) -> (`'F"x) e. ((nei` J)` {A})))
237	236	3ad2antl1 1038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ z e. ((nei` J)` {A})) -> ((z C_ (`'F"x) /\ (`'F"x) C_ X) -> (`'F"x) e. ((nei` J)` {A})))
238	237	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> ((z C_ (`'F"x) /\ (`'F"x) C_ X) -> (`'F"x) e. ((nei` J)` {A})))
239	238	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> (z C_ (`'F"x) -> ((`'F"x) C_ X -> (`'F"x) e. ((nei` J)` {A}))))
240	239	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> ((`'F"x) C_ X -> (z C_ (`'F"x) -> (`'F"x) e. ((nei` J)` {A}))))
241	234, 240	sylbid 220	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> ((`'F"x) C_ (`'F"Y) -> (z C_ (`'F"x) -> (`'F"x) e. ((nei` J)` {A}))))
242		imass2 4299	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x C_ Y -> (`'F"x) C_ (`'F"Y))
243	241, 242	syl5 20	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> (x C_ Y -> (z C_ (`'F"x) -> (`'F"x) e. ((nei` J)` {A}))))
244	243	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> (z C_ (`'F"x) -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A}))))
245		sstr 2625	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((z C_ (`'F"w) /\ (`'F"w) C_ (`'F"x)) -> z C_ (`'F"x))
246	244, 245	syl5 20	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> ((z C_ (`'F"w) /\ (`'F"w) C_ (`'F"x)) -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A}))))
247	246	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> (z C_ (`'F"w) -> ((`'F"w) C_ (`'F"x) -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A})))))
248		imass2 4299	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w C_ x -> (`'F"w) C_ (`'F"x))
249	247, 248	syl7 26	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> (z C_ (`'F"w) -> (w C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A})))))
250	230, 249	sylbid 220	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> ((F"z) C_ w -> (w C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A})))))
251		eqimss 2665	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F"z) = w -> (F"z) C_ w)
252	251	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . 21 |- (w = (F"z) -> (F"z) C_ w)
253	250, 252	syl5 20	. . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ z e. ((nei` J)` {A})) -> (w = (F"z) -> (w C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A})))))
254	253	ex 402	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (z e. ((nei` J)` {A}) -> (w = (F"z) -> (w C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A}))))))
255	254	r19.23adv 2215	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (E.z e. ((nei` J)` {A})w = (F"z) -> (w C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A})))))
256	255	adantr 425	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (E.z e. ((nei` J)` {A})w = (F"z) -> (w C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A})))))
257		sseq1 2637	. . . . . . . . . . . . . . . . . . . 20 |- (w = Y -> (w C_ x <-> Y C_ x))
258	257	adantl 424	. . . . . . . . . . . . . . . . . . 19 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) /\ w = Y) -> (w C_ x <-> Y C_ x))
259	1	tpnei 9010	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (J e. Top -> ({A} C_ X <-> X e. ((nei` J)` {A})))
260	259	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((J e. Top /\ {A} C_ X) -> X e. ((nei` J)` {A}))
261	260, 140	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((J e. Top /\ A e. X) -> X e. ((nei` J)` {A}))
262	261	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ F:X-->Y) /\ A e. X) -> X e. ((nei` J)` {A}))
263	231	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (F:X-->Y -> ((`'F"Y) e. ((nei` J)` {A}) <-> X e. ((nei` J)` {A})))
264	263	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ F:X-->Y) /\ A e. X) -> ((`'F"Y) e. ((nei` J)` {A}) <-> X e. ((nei` J)` {A})))
265	262, 264	mpbird 213	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ F:X-->Y) /\ A e. X) -> (`'F"Y) e. ((nei` J)` {A}))
266	265	3adantl2 1033	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (`'F"Y) e. ((nei` J)` {A}))
267	266	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ Y = x) -> (`'F"Y) e. ((nei` J)` {A}))
268		imaeq2 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (Y = x -> (`'F"Y) = (`'F"x))
269	268	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (Y = x -> ((`'F"Y) e. ((nei` J)` {A}) <-> (`'F"x) e. ((nei` J)` {A})))
270	269	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ Y = x) -> ((`'F"Y) e. ((nei` J)` {A}) <-> (`'F"x) e. ((nei` J)` {A})))
271	267, 270	mpbid 212	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ Y = x) -> (`'F"x) e. ((nei` J)` {A}))
272	271	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (Y = x -> (`'F"x) e. ((nei` J)` {A})))
273	272	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (Y = x -> (`'F"x) e. ((nei` J)` {A})))
274		eqss 2631	. . . . . . . . . . . . . . . . . . . . . . 23 |- (Y = x <-> (Y C_ x /\ x C_ Y))
275	274	bicomi 189	. . . . . . . . . . . . . . . . . . . . . 22 |- ((Y C_ x /\ x C_ Y) <-> Y = x)
276	273, 275	syl5ib 223	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> ((Y C_ x /\ x C_ Y) -> (`'F"x) e. ((nei` J)` {A})))
277	276	exp3a 405	. . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (Y C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A}))))
278	277	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) /\ w = Y) -> (Y C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A}))))
279	258, 278	sylbid 220	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) /\ w = Y) -> (w C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A}))))
280	279	ex 402	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (w = Y -> (w C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A})))))
281	256, 280	jaod 469	. . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> ((E.z e. ((nei` J)` {A})w = (F"z) \/ w = Y) -> (w C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A})))))
282		elun 2741	. . . . . . . . . . . . . . . . 17 |- (w e. ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) <-> (w e. {y | E.z e. ((nei` J)` {A})y = (F"z)} \/ w e. {Y}))
283		visset 2295	. . . . . . . . . . . . . . . . . . 19 |- w e. _V
284		eqeq1 1890	. . . . . . . . . . . . . . . . . . . 20 |- (y = w -> (y = (F"z) <-> w = (F"z)))
285	284	rexbidv 2124	. . . . . . . . . . . . . . . . . . 19 |- (y = w -> (E.z e. ((nei` J)` {A})y = (F"z) <-> E.z e. ((nei` J)` {A})w = (F"z)))
286	283, 285	elab 2403	. . . . . . . . . . . . . . . . . 18 |- (w e. {y | E.z e. ((nei` J)` {A})y = (F"z)} <-> E.z e. ((nei` J)` {A})w = (F"z))
287		elsn 3058	. . . . . . . . . . . . . . . . . 18 |- (w e. {Y} <-> w = Y)
288	286, 287	orbi12i 277	. . . . . . . . . . . . . . . . 17 |- ((w e. {y | E.z e. ((nei` J)` {A})y = (F"z)} \/ w e. {Y}) <-> (E.z e. ((nei` J)` {A})w = (F"z) \/ w = Y))
289	282, 288	bitri 190	. . . . . . . . . . . . . . . 16 |- (w e. ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) <-> (E.z e. ((nei` J)` {A})w = (F"z) \/ w = Y))
290	281, 289	syl5ib 223	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (w e. ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}) -> (w C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A})))))
291	290	r19.23adv 2215	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (E.w e. ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})w C_ x -> (x C_ Y -> (`'F"x) e. ((nei` J)` {A}))))
292	291	com23 36	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (x C_ Y -> (E.w e. ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})w C_ x -> (`'F"x) e. ((nei` J)` {A}))))
293	292	imp3a 388	. . . . . . . . . . . 12 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> ((x C_ Y /\ E.w e. ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})w C_ x) -> (`'F"x) e. ((nei` J)` {A})))
294	218, 293	sylbid 220	. . . . . . . . . . 11 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (x e. (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})) -> (`'F"x) e. ((nei` J)` {A})))
295	294	a1d 15	. . . . . . . . . 10 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (x e. ((nei` K)` {(F` A)}) -> (x e. (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})) -> (`'F"x) e. ((nei` J)` {A}))))
296	213, 295	mpdd 57	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (x e. ((nei` K)` {(F` A)}) -> (`'F"x) e. ((nei` J)` {A})))
297	296	r19.21aiv 2175	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) /\ (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}))
298	297	expcom 403	. . . . . . 7 |- ((F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y}))) -> (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})))
299	168, 298	syl6 25	. . . . . 6 |- ((X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A}))) -> (((X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A}))) -> (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}))))
300	299	com3r 39	. . . . 5 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> ((X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A}))) -> (((X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A}))) -> (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}))))
301	167, 300	mpd 29	. . . 4 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (((X = U.((nei` J)` {A}) /\ A e. ((fLim1` J)` ((nei` J)` {A}))) -> (F` A) e. ((fLim1` K)` (filGen` ({y | E.z e. ((nei` J)` {A})y = (F"z)} u. {Y})))) -> A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})))
302	161, 301	syld 30	. . 3 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.f e. Fil ((X = U.f /\ A e. ((fLim1` J)` f)) -> (F` A) e. ((fLim1` K)` L)) -> A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A})))
303	138, 302	impbid 574	. 2 |- (((J e. Top /\ K e. Top /\ F:X-->Y) /\ A e. X) -> (A.x e. ((nei` K)` {(F` A)})(`'F"x) e. ((nei` J)` {A}) <-> A.f e. Fil ((X = U.f /\ A e. ((fLim1` J)` f)) -> (F` A) e. ((fLim1` K)` L))))
304	3, 303	bitrd 587	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. ((fLim1` J)` f)) -> (F` A) e. ((fLim1` K)` L))))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   u. cun 2591   C_ wss 2593  (/)c0 2875  {csn 3044  U.cuni 3177  U_ciun 3255  `'ccnv 3985  dom cdm 3986  ran crn 3987  "cima 3989  Fun wfun 3992   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  Topctop 8857  neicnei 8988   CnP ccnp 9029  fBascfbas 10257  filGencfg 10258  Filcfil 10264  fLim1cflim1 10294

This theorem is referenced by:  cnfillim 15590  flimfcnp 15602  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-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-iun 3257  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-nei 8989  df-cnp 9031  df-fbas 10259  df-fg 10260  df-fil 10265  df-flim1 10295

Copyright terms: Public domain