Theorem limfilcf 15587

Description: Fineness is properly characterized by the property that every limit point of a filter in the finer topology is a limit point in the coarser topology. (Contributed by Jeff Hankins, 28-Sep-2009.)

Hypotheses

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

Assertion

Ref	Expression
limfilcf	|- ((J e. Top /\ K e. Top /\ X = Y) -> (J C_ K <-> A.f e. Fil (X = U.f -> ((fLim1` K)` f) C_ ((fLim1` J)` f))))

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

Proof of Theorem limfilcf

Step	Hyp	Ref	Expression
1		limfilcf.1	. . 3 |- X = U.J
2		limfilcf.2	. . 3 |- Y = U.K
3	1, 2	topfne 15500	. 2 |- ((J e. Top /\ K e. Top /\ X = Y) -> (J C_ K <-> JFneK))
4		eleq2 1958	. . . . . . . . . . . 12 |- (X = Y -> (x e. X <-> x e. Y))
5	4	biimprd 171	. . . . . . . . . . 11 |- (X = Y -> (x e. Y -> x e. X))
6	5	3ad2ant3 899	. . . . . . . . . 10 |- ((J e. Top /\ K e. Top /\ X = Y) -> (x e. Y -> x e. X))
7	6	ad2antrr 440	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) -> (x e. Y -> x e. X))
8		elssuni 3206	. . . . . . . . . . . . . . . 16 |- (o e. J -> o C_ U.J)
9	8, 1	syl6ssr 2664	. . . . . . . . . . . . . . 15 |- (o e. J -> o C_ X)
10	9	ad2antll 443	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ (x e. o /\ o e. J)) -> o C_ X)
11		simp2 877	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ K e. Top /\ X = Y) -> K e. Top)
12	11	adantr 425	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) -> K e. Top)
13	12	ad2antrr 440	. . . . . . . . . . . . . . 15 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ (x e. o /\ o e. J)) -> K e. Top)
14		simpllr 453	. . . . . . . . . . . . . . 15 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ (x e. o /\ o e. J)) -> JFneK)
15		simprr 451	. . . . . . . . . . . . . . 15 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ (x e. o /\ o e. J)) -> o e. J)
16		simprl 450	. . . . . . . . . . . . . . 15 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ (x e. o /\ o e. J)) -> x e. o)
17		fnessex 15484	. . . . . . . . . . . . . . 15 |- (((K e. Top /\ JFneK /\ o e. J) /\ x e. o) -> E.p e. K (x e. p /\ p C_ o))
18	13, 14, 15, 16, 17	syl31anc 1103	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ (x e. o /\ o e. J)) -> E.p e. K (x e. p /\ p C_ o))
19	10, 18	jca 310	. . . . . . . . . . . . 13 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ (x e. o /\ o e. J)) -> (o C_ X /\ E.p e. K (x e. p /\ p C_ o)))
20		ax-17 1317	. . . . . . . . . . . . . . 15 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ o C_ X) -> A.p((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ o C_ X))
21		hbra1 2147	. . . . . . . . . . . . . . . 16 |- (A.p e. K (x e. p -> p e. f) -> A.pA.p e. K (x e. p -> p e. f))
22		ax-17 1317	. . . . . . . . . . . . . . . 16 |- (o e. f -> A.p o e. f)
23	21, 22	hbim 1354	. . . . . . . . . . . . . . 15 |- ((A.p e. K (x e. p -> p e. f) -> o e. f) -> A.p(A.p e. K (x e. p -> p e. f) -> o e. f))
24		ra4 2155	. . . . . . . . . . . . . . . . 17 |- (A.p e. K (x e. p -> p e. f) -> (p e. K -> (x e. p -> p e. f)))
25		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (X = U.f -> (o C_ X <-> o C_ U.f))
26	25	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((X = U.f /\ o C_ X) -> o C_ U.f)
27	26	adantll 428	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f e. Fil /\ X = U.f) /\ o C_ X) -> o C_ U.f)
28		simpll 448	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((f e. Fil /\ o C_ U.f) /\ (p C_ o /\ p e. f)) -> f e. Fil)
29		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((f e. Fil /\ o C_ U.f) /\ (p C_ o /\ p e. f)) -> p e. f)
30		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((f e. Fil /\ o C_ U.f) /\ (p C_ o /\ p e. f)) -> o C_ U.f)
31		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((f e. Fil /\ o C_ U.f) /\ (p C_ o /\ p e. f)) -> p C_ o)
32	29, 30, 31	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((f e. Fil /\ o C_ U.f) /\ (p C_ o /\ p e. f)) -> (p e. f /\ o C_ U.f /\ p C_ o))
33		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- U.f = U.f
34	33	fillsb 10270	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f e. Fil -> ((p e. f /\ o C_ U.f /\ p C_ o) -> o e. f))
35	28, 32, 34	sylc 83	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((f e. Fil /\ o C_ U.f) /\ (p C_ o /\ p e. f)) -> o e. f)
36	35	exp32 408	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f e. Fil /\ o C_ U.f) -> (p C_ o -> (p e. f -> o e. f)))
37	36	adantlr 429	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f e. Fil /\ X = U.f) /\ o C_ U.f) -> (p C_ o -> (p e. f -> o e. f)))
38	27, 37	syldan 516	. . . . . . . . . . . . . . . . . . . . 21 |- (((f e. Fil /\ X = U.f) /\ o C_ X) -> (p C_ o -> (p e. f -> o e. f)))
39	38	adantll 428	. . . . . . . . . . . . . . . . . . . 20 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ o C_ X) -> (p C_ o -> (p e. f -> o e. f)))
40	39	com13 37	. . . . . . . . . . . . . . . . . . 19 |- (p e. f -> (p C_ o -> (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ o C_ X) -> o e. f)))
41	40	imim2i 11	. . . . . . . . . . . . . . . . . 18 |- ((x e. p -> p e. f) -> (x e. p -> (p C_ o -> (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ o C_ X) -> o e. f))))
42	41	imp3a 388	. . . . . . . . . . . . . . . . 17 |- ((x e. p -> p e. f) -> ((x e. p /\ p C_ o) -> (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ o C_ X) -> o e. f)))
43	24, 42	syl6 25	. . . . . . . . . . . . . . . 16 |- (A.p e. K (x e. p -> p e. f) -> (p e. K -> ((x e. p /\ p C_ o) -> (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ o C_ X) -> o e. f))))
44	43	com14 42	. . . . . . . . . . . . . . 15 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ o C_ X) -> (p e. K -> ((x e. p /\ p C_ o) -> (A.p e. K (x e. p -> p e. f) -> o e. f))))
45	20, 23, 44	r19.23ad 2213	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ o C_ X) -> (E.p e. K (x e. p /\ p C_ o) -> (A.p e. K (x e. p -> p e. f) -> o e. f)))
46	45	impr 422	. . . . . . . . . . . . 13 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ (o C_ X /\ E.p e. K (x e. p /\ p C_ o))) -> (A.p e. K (x e. p -> p e. f) -> o e. f))
47	19, 46	syldan 516	. . . . . . . . . . . 12 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) /\ (x e. o /\ o e. J)) -> (A.p e. K (x e. p -> p e. f) -> o e. f))
48	47	exp32 408	. . . . . . . . . . 11 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) -> (x e. o -> (o e. J -> (A.p e. K (x e. p -> p e. f) -> o e. f))))
49	48	com24 41	. . . . . . . . . 10 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) -> (A.p e. K (x e. p -> p e. f) -> (o e. J -> (x e. o -> o e. f))))
50	49	r19.21adv 2181	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) -> (A.p e. K (x e. p -> p e. f) -> A.o e. J (x e. o -> o e. f)))
51	7, 50	anim12d 617	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) -> ((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f))))
52	51	19.21aiv 1664	. . . . . . 7 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (f e. Fil /\ X = U.f)) -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f))))
53	52	expr 418	. . . . . 6 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ f e. Fil) -> (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f)))))
54	53	r19.21aiva 2176	. . . . 5 |- (((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) -> A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f)))))
55	1, 2	isfne2 15481	. . . . . . . 8 |- (K e. Top -> (JFneK <-> (X = Y /\ A.q e. J A.y e. q E.r e. K (y e. r /\ r C_ q))))
56	55	3ad2ant2 898	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ X = Y) -> (JFneK <-> (X = Y /\ A.q e. J A.y e. q E.r e. K (y e. r /\ r C_ q))))
57	56	adantr 425	. . . . . 6 |- (((J e. Top /\ K e. Top /\ X = Y) /\ A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f))))) -> (JFneK <-> (X = Y /\ A.q e. J A.y e. q E.r e. K (y e. r /\ r C_ q))))
58		simp3 878	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ X = Y) -> X = Y)
59	58	adantr 425	. . . . . 6 |- (((J e. Top /\ K e. Top /\ X = Y) /\ A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f))))) -> X = Y)
60	11	adantr 425	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> K e. Top)
61		sseq2 2639	. . . . . . . . . . . . . . . 16 |- (X = Y -> ({y} C_ X <-> {y} C_ Y))
62	61	biimpa 460	. . . . . . . . . . . . . . 15 |- ((X = Y /\ {y} C_ X) -> {y} C_ Y)
63	62	3ad2antl3 1040	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ X = Y) /\ {y} C_ X) -> {y} C_ Y)
64		snssi 3129	. . . . . . . . . . . . . . 15 |- (y e. q -> {y} C_ q)
65		elssuni 3206	. . . . . . . . . . . . . . . 16 |- (q e. J -> q C_ U.J)
66	65, 1	syl6ssr 2664	. . . . . . . . . . . . . . 15 |- (q e. J -> q C_ X)
67	64, 66	sylan9ssr 2630	. . . . . . . . . . . . . 14 |- ((q e. J /\ y e. q) -> {y} C_ X)
68	63, 67	sylan2 500	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> {y} C_ Y)
69		visset 2295	. . . . . . . . . . . . . . 15 |- y e. _V
70	69	snnz 3119	. . . . . . . . . . . . . 14 |- {y} =/= (/)
71	70	a1i 8	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> {y} =/= (/))
72	2	neifil 10302	. . . . . . . . . . . . 13 |- ((K e. Top /\ {y} C_ Y /\ {y} =/= (/)) -> ((nei` K)` {y}) e. Fil)
73	60, 68, 71, 72	syl111anc 1100	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> ((nei` K)` {y}) e. Fil)
74		unieq 3185	. . . . . . . . . . . . . . 15 |- (f = ((nei` K)` {y}) -> U.f = U.((nei` K)` {y}))
75	74	eqeq2d 1895	. . . . . . . . . . . . . 14 |- (f = ((nei` K)` {y}) -> (X = U.f <-> X = U.((nei` K)` {y})))
76		eleq2 1958	. . . . . . . . . . . . . . . . . . 19 |- (f = ((nei` K)` {y}) -> (p e. f <-> p e. ((nei` K)` {y})))
77	76	imbi2d 674	. . . . . . . . . . . . . . . . . 18 |- (f = ((nei` K)` {y}) -> ((x e. p -> p e. f) <-> (x e. p -> p e. ((nei` K)` {y}))))
78	77	ralbidv 2123	. . . . . . . . . . . . . . . . 17 |- (f = ((nei` K)` {y}) -> (A.p e. K (x e. p -> p e. f) <-> A.p e. K (x e. p -> p e. ((nei` K)` {y}))))
79	78	anbi2d 678	. . . . . . . . . . . . . . . 16 |- (f = ((nei` K)` {y}) -> ((x e. Y /\ A.p e. K (x e. p -> p e. f)) <-> (x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y})))))
80		eleq2 1958	. . . . . . . . . . . . . . . . . . 19 |- (f = ((nei` K)` {y}) -> (o e. f <-> o e. ((nei` K)` {y})))
81	80	imbi2d 674	. . . . . . . . . . . . . . . . . 18 |- (f = ((nei` K)` {y}) -> ((x e. o -> o e. f) <-> (x e. o -> o e. ((nei` K)` {y}))))
82	81	ralbidv 2123	. . . . . . . . . . . . . . . . 17 |- (f = ((nei` K)` {y}) -> (A.o e. J (x e. o -> o e. f) <-> A.o e. J (x e. o -> o e. ((nei` K)` {y}))))
83	82	anbi2d 678	. . . . . . . . . . . . . . . 16 |- (f = ((nei` K)` {y}) -> ((x e. X /\ A.o e. J (x e. o -> o e. f)) <-> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y})))))
84	79, 83	imbi12d 688	. . . . . . . . . . . . . . 15 |- (f = ((nei` K)` {y}) -> (((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f))) <-> ((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) -> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y}))))))
85	84	albidv 1656	. . . . . . . . . . . . . 14 |- (f = ((nei` K)` {y}) -> (A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f))) <-> A.x((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) -> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y}))))))
86	75, 85	imbi12d 688	. . . . . . . . . . . . 13 |- (f = ((nei` K)` {y}) -> ((X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f)))) <-> (X = U.((nei` K)` {y}) -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) -> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y})))))))
87	86	rcla4v 2376	. . . . . . . . . . . 12 |- (((nei` K)` {y}) e. Fil -> (A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f)))) -> (X = U.((nei` K)` {y}) -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) -> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y})))))))
88	73, 87	syl 12	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> (A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f)))) -> (X = U.((nei` K)` {y}) -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) -> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y})))))))
89	58	adantr 425	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> X = Y)
90	2	unnei 9011	. . . . . . . . . . . . . . . 16 |- ((K e. Top /\ {y} C_ Y) -> U.((nei` K)` {y}) = Y)
91	90	3ad2antl2 1039	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ X = Y) /\ {y} C_ Y) -> U.((nei` K)` {y}) = Y)
92	63, 91	syldan 516	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ X = Y) /\ {y} C_ X) -> U.((nei` K)` {y}) = Y)
93	92, 67	sylan2 500	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> U.((nei` K)` {y}) = Y)
94	89, 93	eqtr4d 1928	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> X = U.((nei` K)` {y}))
95		pm2.27 76	. . . . . . . . . . . . 13 |- (X = U.((nei` K)` {y}) -> ((X = U.((nei` K)` {y}) -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) -> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y}))))) -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) -> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y}))))))
96		ssel2 2616	. . . . . . . . . . . . . . . . . 18 |- ((q C_ X /\ y e. q) -> y e. X)
97	96, 66	sylan 497	. . . . . . . . . . . . . . . . 17 |- ((q e. J /\ y e. q) -> y e. X)
98	97	adantl 424	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> y e. X)
99	98, 89	eleqtrd 1973	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> y e. Y)
100		simpll2 916	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) /\ (p e. K /\ y e. p)) -> K e. Top)
101		simprl 450	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) /\ (p e. K /\ y e. p)) -> p e. K)
102		simprr 451	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) /\ (p e. K /\ y e. p)) -> y e. p)
103		opnneip 9009	. . . . . . . . . . . . . . . . . 18 |- ((K e. Top /\ p e. K /\ y e. p) -> p e. ((nei` K)` {y}))
104	100, 101, 102, 103	syl111anc 1100	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) /\ (p e. K /\ y e. p)) -> p e. ((nei` K)` {y}))
105	104	expr 418	. . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) /\ p e. K) -> (y e. p -> p e. ((nei` K)` {y})))
106	105	r19.21aiva 2176	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> A.p e. K (y e. p -> p e. ((nei` K)` {y})))
107		pm2.27 76	. . . . . . . . . . . . . . . 16 |- ((y e. Y /\ A.p e. K (y e. p -> p e. ((nei` K)` {y}))) -> (((y e. Y /\ A.p e. K (y e. p -> p e. ((nei` K)` {y}))) -> (y e. X /\ A.o e. J (y e. o -> o e. ((nei` K)` {y})))) -> (y e. X /\ A.o e. J (y e. o -> o e. ((nei` K)` {y})))))
108		eleq2 1958	. . . . . . . . . . . . . . . . . . . . 21 |- (o = q -> (y e. o <-> y e. q))
109		eleq1 1957	. . . . . . . . . . . . . . . . . . . . 21 |- (o = q -> (o e. ((nei` K)` {y}) <-> q e. ((nei` K)` {y})))
110	108, 109	imbi12d 688	. . . . . . . . . . . . . . . . . . . 20 |- (o = q -> ((y e. o -> o e. ((nei` K)` {y})) <-> (y e. q -> q e. ((nei` K)` {y}))))
111	110	rcla4v 2376	. . . . . . . . . . . . . . . . . . 19 |- (q e. J -> (A.o e. J (y e. o -> o e. ((nei` K)` {y})) -> (y e. q -> q e. ((nei` K)` {y}))))
112	111	ad2antrl 442	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> (A.o e. J (y e. o -> o e. ((nei` K)` {y})) -> (y e. q -> q e. ((nei` K)` {y}))))
113		pm2.27 76	. . . . . . . . . . . . . . . . . . . 20 |- (y e. q -> ((y e. q -> q e. ((nei` K)` {y})) -> q e. ((nei` K)` {y})))
114		neii2 8998	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((K e. Top /\ q e. ((nei` K)` {y})) -> E.r e. K ({y} C_ r /\ r C_ q))
115	69	snss 3122	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. r <-> {y} C_ r)
116	115	anbi1i 539	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((y e. r /\ r C_ q) <-> ({y} C_ r /\ r C_ q))
117	116	rexbii 2128	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (E.r e. K (y e. r /\ r C_ q) <-> E.r e. K ({y} C_ r /\ r C_ q))
118	114, 117	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((K e. Top /\ q e. ((nei` K)` {y})) -> E.r e. K (y e. r /\ r C_ q))
119	118	ex 402	. . . . . . . . . . . . . . . . . . . . . 22 |- (K e. Top -> (q e. ((nei` K)` {y}) -> E.r e. K (y e. r /\ r C_ q)))
120	119	3ad2ant2 898	. . . . . . . . . . . . . . . . . . . . 21 |- ((J e. Top /\ K e. Top /\ X = Y) -> (q e. ((nei` K)` {y}) -> E.r e. K (y e. r /\ r C_ q)))
121	120	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ K e. Top /\ X = Y) /\ q e. J) -> (q e. ((nei` K)` {y}) -> E.r e. K (y e. r /\ r C_ q)))
122	113, 121	syl9r 72	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ K e. Top /\ X = Y) /\ q e. J) -> (y e. q -> ((y e. q -> q e. ((nei` K)` {y})) -> E.r e. K (y e. r /\ r C_ q))))
123	122	impr 422	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> ((y e. q -> q e. ((nei` K)` {y})) -> E.r e. K (y e. r /\ r C_ q)))
124	112, 123	syld 30	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> (A.o e. J (y e. o -> o e. ((nei` K)` {y})) -> E.r e. K (y e. r /\ r C_ q)))
125	124	adantld 426	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> ((y e. X /\ A.o e. J (y e. o -> o e. ((nei` K)` {y}))) -> E.r e. K (y e. r /\ r C_ q)))
126	107, 125	syl9r 72	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> ((y e. Y /\ A.p e. K (y e. p -> p e. ((nei` K)` {y}))) -> (((y e. Y /\ A.p e. K (y e. p -> p e. ((nei` K)` {y}))) -> (y e. X /\ A.o e. J (y e. o -> o e. ((nei` K)` {y})))) -> E.r e. K (y e. r /\ r C_ q))))
127	99, 106, 126	mp2and 767	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> (((y e. Y /\ A.p e. K (y e. p -> p e. ((nei` K)` {y}))) -> (y e. X /\ A.o e. J (y e. o -> o e. ((nei` K)` {y})))) -> E.r e. K (y e. r /\ r C_ q)))
128		eleq1 1957	. . . . . . . . . . . . . . . . 17 |- (x = y -> (x e. Y <-> y e. Y))
129		eleq1 1957	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> (x e. p <-> y e. p))
130	129	imbi1d 675	. . . . . . . . . . . . . . . . . 18 |- (x = y -> ((x e. p -> p e. ((nei` K)` {y})) <-> (y e. p -> p e. ((nei` K)` {y}))))
131	130	ralbidv 2123	. . . . . . . . . . . . . . . . 17 |- (x = y -> (A.p e. K (x e. p -> p e. ((nei` K)` {y})) <-> A.p e. K (y e. p -> p e. ((nei` K)` {y}))))
132	128, 131	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (x = y -> ((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) <-> (y e. Y /\ A.p e. K (y e. p -> p e. ((nei` K)` {y})))))
133		eleq1 1957	. . . . . . . . . . . . . . . . 17 |- (x = y -> (x e. X <-> y e. X))
134		eleq1 1957	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> (x e. o <-> y e. o))
135	134	imbi1d 675	. . . . . . . . . . . . . . . . . 18 |- (x = y -> ((x e. o -> o e. ((nei` K)` {y})) <-> (y e. o -> o e. ((nei` K)` {y}))))
136	135	ralbidv 2123	. . . . . . . . . . . . . . . . 17 |- (x = y -> (A.o e. J (x e. o -> o e. ((nei` K)` {y})) <-> A.o e. J (y e. o -> o e. ((nei` K)` {y}))))
137	133, 136	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (x = y -> ((x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y}))) <-> (y e. X /\ A.o e. J (y e. o -> o e. ((nei` K)` {y})))))
138	132, 137	imbi12d 688	. . . . . . . . . . . . . . 15 |- (x = y -> (((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) -> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y})))) <-> ((y e. Y /\ A.p e. K (y e. p -> p e. ((nei` K)` {y}))) -> (y e. X /\ A.o e. J (y e. o -> o e. ((nei` K)` {y}))))))
139	138	a4v 1649	. . . . . . . . . . . . . 14 |- (A.x((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) -> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y})))) -> ((y e. Y /\ A.p e. K (y e. p -> p e. ((nei` K)` {y}))) -> (y e. X /\ A.o e. J (y e. o -> o e. ((nei` K)` {y})))))
140	127, 139	syl5 20	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> (A.x((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) -> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y})))) -> E.r e. K (y e. r /\ r C_ q)))
141	95, 140	syl9r 72	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> (X = U.((nei` K)` {y}) -> ((X = U.((nei` K)` {y}) -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) -> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y}))))) -> E.r e. K (y e. r /\ r C_ q))))
142	94, 141	mpd 29	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> ((X = U.((nei` K)` {y}) -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. ((nei` K)` {y}))) -> (x e. X /\ A.o e. J (x e. o -> o e. ((nei` K)` {y}))))) -> E.r e. K (y e. r /\ r C_ q)))
143	88, 142	syld 30	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (q e. J /\ y e. q)) -> (A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f)))) -> E.r e. K (y e. r /\ r C_ q)))
144	143	ex 402	. . . . . . . . 9 |- ((J e. Top /\ K e. Top /\ X = Y) -> ((q e. J /\ y e. q) -> (A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f)))) -> E.r e. K (y e. r /\ r C_ q))))
145	144	com23 36	. . . . . . . 8 |- ((J e. Top /\ K e. Top /\ X = Y) -> (A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f)))) -> ((q e. J /\ y e. q) -> E.r e. K (y e. r /\ r C_ q))))
146	145	imp 377	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ X = Y) /\ A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f))))) -> ((q e. J /\ y e. q) -> E.r e. K (y e. r /\ r C_ q)))
147	146	r19.21aivv 2183	. . . . . 6 |- (((J e. Top /\ K e. Top /\ X = Y) /\ A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f))))) -> A.q e. J A.y e. q E.r e. K (y e. r /\ r C_ q))
148	57, 59, 147	mpbir2and 802	. . . . 5 |- (((J e. Top /\ K e. Top /\ X = Y) /\ A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f))))) -> JFneK)
149	54, 148	impbida 577	. . . 4 |- ((J e. Top /\ K e. Top /\ X = Y) -> (JFneK <-> A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f))))))
150		eqtr2 1905	. . . . . . . . . . 11 |- ((X = Y /\ X = U.f) -> Y = U.f)
151	150	3ad2antl3 1040	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ X = Y) /\ X = U.f) -> Y = U.f)
152	151	adantlr 429	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ f e. Fil) /\ X = U.f) -> Y = U.f)
153		simpl 346	. . . . . . . . . . . . . . 15 |- (((K e. Top /\ f e. Fil /\ Y = U.f) /\ x e. ((fLim1` K)` f)) -> (K e. Top /\ f e. Fil /\ Y = U.f))
154	2, 33	flimelbas 10300	. . . . . . . . . . . . . . 15 |- (((K e. Top /\ f e. Fil /\ Y = U.f) /\ x e. ((fLim1` K)` f)) -> x e. Y)
155	153, 154	jca 310	. . . . . . . . . . . . . 14 |- (((K e. Top /\ f e. Fil /\ Y = U.f) /\ x e. ((fLim1` K)` f)) -> ((K e. Top /\ f e. Fil /\ Y = U.f) /\ x e. Y))
156		simpl 346	. . . . . . . . . . . . . . 15 |- ((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> x e. Y)
157	156	anim2i 362	. . . . . . . . . . . . . 14 |- (((K e. Top /\ f e. Fil /\ Y = U.f) /\ (x e. Y /\ A.p e. K (x e. p -> p e. f))) -> ((K e. Top /\ f e. Fil /\ Y = U.f) /\ x e. Y))
158	2, 33	flimopn 10321	. . . . . . . . . . . . . . 15 |- (((K e. Top /\ f e. Fil /\ Y = U.f) /\ x e. Y) -> (x e. ((fLim1` K)` f) <-> A.p e. K (x e. p -> p e. f)))
159		ibar 705	. . . . . . . . . . . . . . . 16 |- (x e. Y -> (A.p e. K (x e. p -> p e. f) <-> (x e. Y /\ A.p e. K (x e. p -> p e. f))))
160	159	adantl 424	. . . . . . . . . . . . . . 15 |- (((K e. Top /\ f e. Fil /\ Y = U.f) /\ x e. Y) -> (A.p e. K (x e. p -> p e. f) <-> (x e. Y /\ A.p e. K (x e. p -> p e. f))))
161	158, 160	bitrd 587	. . . . . . . . . . . . . 14 |- (((K e. Top /\ f e. Fil /\ Y = U.f) /\ x e. Y) -> (x e. ((fLim1` K)` f) <-> (x e. Y /\ A.p e. K (x e. p -> p e. f))))
162	155, 157, 161	pm5.21nd 744	. . . . . . . . . . . . 13 |- ((K e. Top /\ f e. Fil /\ Y = U.f) -> (x e. ((fLim1` K)` f) <-> (x e. Y /\ A.p e. K (x e. p -> p e. f))))
163	162	bicomd 580	. . . . . . . . . . . 12 |- ((K e. Top /\ f e. Fil /\ Y = U.f) -> ((x e. Y /\ A.p e. K (x e. p -> p e. f)) <-> x e. ((fLim1` K)` f)))
164	163	3expb 1068	. . . . . . . . . . 11 |- ((K e. Top /\ (f e. Fil /\ Y = U.f)) -> ((x e. Y /\ A.p e. K (x e. p -> p e. f)) <-> x e. ((fLim1` K)` f)))
165	164	3ad2antl2 1039	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ Y = U.f)) -> ((x e. Y /\ A.p e. K (x e. p -> p e. f)) <-> x e. ((fLim1` K)` f)))
166	165	anassrs 489	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ f e. Fil) /\ Y = U.f) -> ((x e. Y /\ A.p e. K (x e. p -> p e. f)) <-> x e. ((fLim1` K)` f)))
167	152, 166	syldan 516	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ f e. Fil) /\ X = U.f) -> ((x e. Y /\ A.p e. K (x e. p -> p e. f)) <-> x e. ((fLim1` K)` f)))
168		simpl 346	. . . . . . . . . . . . . 14 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ x e. ((fLim1` J)` f)) -> (J e. Top /\ f e. Fil /\ X = U.f))
169	1, 33	flimelbas 10300	. . . . . . . . . . . . . 14 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ x e. ((fLim1` J)` f)) -> x e. X)
170	168, 169	jca 310	. . . . . . . . . . . . 13 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ x e. ((fLim1` J)` f)) -> ((J e. Top /\ f e. Fil /\ X = U.f) /\ x e. X))
171		simpl 346	. . . . . . . . . . . . . 14 |- ((x e. X /\ A.o e. J (x e. o -> o e. f)) -> x e. X)
172	171	anim2i 362	. . . . . . . . . . . . 13 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ (x e. X /\ A.o e. J (x e. o -> o e. f))) -> ((J e. Top /\ f e. Fil /\ X = U.f) /\ x e. X))
173	1, 33	flimopn 10321	. . . . . . . . . . . . . 14 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ x e. X) -> (x e. ((fLim1` J)` f) <-> A.o e. J (x e. o -> o e. f)))
174		ibar 705	. . . . . . . . . . . . . . 15 |- (x e. X -> (A.o e. J (x e. o -> o e. f) <-> (x e. X /\ A.o e. J (x e. o -> o e. f))))
175	174	adantl 424	. . . . . . . . . . . . . 14 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ x e. X) -> (A.o e. J (x e. o -> o e. f) <-> (x e. X /\ A.o e. J (x e. o -> o e. f))))
176	173, 175	bitrd 587	. . . . . . . . . . . . 13 |- (((J e. Top /\ f e. Fil /\ X = U.f) /\ x e. X) -> (x e. ((fLim1` J)` f) <-> (x e. X /\ A.o e. J (x e. o -> o e. f))))
177	170, 172, 176	pm5.21nd 744	. . . . . . . . . . . 12 |- ((J e. Top /\ f e. Fil /\ X = U.f) -> (x e. ((fLim1` J)` f) <-> (x e. X /\ A.o e. J (x e. o -> o e. f))))
178	177	3expb 1068	. . . . . . . . . . 11 |- ((J e. Top /\ (f e. Fil /\ X = U.f)) -> (x e. ((fLim1` J)` f) <-> (x e. X /\ A.o e. J (x e. o -> o e. f))))
179	178	3ad2antl1 1038	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> (x e. ((fLim1` J)` f) <-> (x e. X /\ A.o e. J (x e. o -> o e. f))))
180	179	anassrs 489	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ f e. Fil) /\ X = U.f) -> (x e. ((fLim1` J)` f) <-> (x e. X /\ A.o e. J (x e. o -> o e. f))))
181	180	bicomd 580	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ f e. Fil) /\ X = U.f) -> ((x e. X /\ A.o e. J (x e. o -> o e. f)) <-> x e. ((fLim1` J)` f)))
182	167, 181	imbi12d 688	. . . . . . 7 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ f e. Fil) /\ X = U.f) -> (((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f))) <-> (x e. ((fLim1` K)` f) -> x e. ((fLim1` J)` f))))
183	182	albidv 1656	. . . . . 6 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ f e. Fil) /\ X = U.f) -> (A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f))) <-> A.x(x e. ((fLim1` K)` f) -> x e. ((fLim1` J)` f))))
184	183	pm5.74da 646	. . . . 5 |- (((J e. Top /\ K e. Top /\ X = Y) /\ f e. Fil) -> ((X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f)))) <-> (X = U.f -> A.x(x e. ((fLim1` K)` f) -> x e. ((fLim1` J)` f)))))
185	184	ralbidva 2119	. . . 4 |- ((J e. Top /\ K e. Top /\ X = Y) -> (A.f e. Fil (X = U.f -> A.x((x e. Y /\ A.p e. K (x e. p -> p e. f)) -> (x e. X /\ A.o e. J (x e. o -> o e. f)))) <-> A.f e. Fil (X = U.f -> A.x(x e. ((fLim1` K)` f) -> x e. ((fLim1` J)` f)))))
186	149, 185	bitrd 587	. . 3 |- ((J e. Top /\ K e. Top /\ X = Y) -> (JFneK <-> A.f e. Fil (X = U.f -> A.x(x e. ((fLim1` K)` f) -> x e. ((fLim1` J)` f)))))
187		dfss2 2610	. . . . 5 |- (((fLim1` K)` f) C_ ((fLim1` J)` f) <-> A.x(x e. ((fLim1` K)` f) -> x e. ((fLim1` J)` f)))
188	187	imbi2i 202	. . . 4 |- ((X = U.f -> ((fLim1` K)` f) C_ ((fLim1` J)` f)) <-> (X = U.f -> A.x(x e. ((fLim1` K)` f) -> x e. ((fLim1` J)` f))))
189	188	ralbii 2127	. . 3 |- (A.f e. Fil (X = U.f -> ((fLim1` K)` f) C_ ((fLim1` J)` f)) <-> A.f e. Fil (X = U.f -> A.x(x e. ((fLim1` K)` f) -> x e. ((fLim1` J)` f))))
190	186, 189	syl6bbr 597	. 2 |- ((J e. Top /\ K e. Top /\ X = Y) -> (JFneK <-> A.f e. Fil (X = U.f -> ((fLim1` K)` f) C_ ((fLim1` J)` f))))
191	3, 190	bitrd 587	1 |- ((J e. Top /\ K e. Top /\ X = Y) -> (J C_ K <-> A.f e. Fil (X = U.f -> ((fLim1` K)` f) C_ ((fLim1` J)` f))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106   C_ wss 2593  (/)c0 2875  {csn 3044  U.cuni 3177   class class class wbr 3338  ` cfv 3998  Topctop 8857  neicnei 8988  Filcfil 10264  fLim1cflim1 10294  Fnecfne 15457

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

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

Copyright terms: Public domain