Theorem conttnf 14944

Description: F is continous at point A iff a limit of F when x tends to A is (F` A). Bourbaki TG I.50 prop. 9.

Hypotheses

Ref	Expression
conttnf.1	|- L = ((nei` J)` {A})
conttnf.2	|- X = U.K
conttnf.3	|- Y = U.J

Assertion

Ref	Expression
conttnf	|- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> (F e. ((J CnP K)` A) <-> (F` A) e. ((K fLimf L)` F)))

Proof of Theorem conttnf

Step	Hyp	Ref	Expression
1		ffvelrn 4787	. . . . 5 |- ((F:Y-->X /\ A e. Y) -> (F` A) e. X)
2	1	ancoms 484	. . . 4 |- ((A e. Y /\ F:Y-->X) -> (F` A) e. X)
3	2	3ad2ant3 899	. . 3 |- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> (F` A) e. X)
4	3	biantrurd 796	. 2 |- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> (A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o) <-> ((F` A) e. X /\ A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o))))
5		conttnf.3	. . . . . . . . 9 |- Y = U.J
6		conttnf.2	. . . . . . . . 9 |- X = U.K
7	5, 6	iscnp 9036	. . . . . . . 8 |- ((J e. Top /\ K e. Top /\ A e. Y) -> (F e. ((J CnP K)` A) <-> (F:Y-->X /\ A.o e. K ((F` A) e. o -> E.x e. J (A e. x /\ (F"x) C_ o)))))
8		elssuni 3206	. . . . . . . . . . . . . . . . 17 |- (o e. K -> o C_ U.K)
9	6	eqcomi 1888	. . . . . . . . . . . . . . . . . . 19 |- U.K = X
10	9	sseq2i 2642	. . . . . . . . . . . . . . . . . 18 |- (o C_ U.K <-> o C_ X)
11		opnneip 9009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((J e. Top /\ x e. J /\ A e. x) -> x e. ((nei` J)` {A}))
12		conttnf.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- L = ((nei` J)` {A})
13	12	eleq2i 1961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (x e. L <-> x e. ((nei` J)` {A}))
14		imaeq2 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (v = x -> (F"v) = (F"x))
15	14	sseq1d 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (v = x -> ((F"v) C_ o <-> (F"x) C_ o))
16	15	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((x e. L /\ (F"x) C_ o) -> E.v e. L (F"v) C_ o)
17	16	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (x e. L -> ((F"x) C_ o -> E.v e. L (F"v) C_ o))
18	13, 17	sylbir 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (x e. ((nei` J)` {A}) -> ((F"x) C_ o -> E.v e. L (F"v) C_ o))
19	18	a1dd 53	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (x e. ((nei` J)` {A}) -> ((F"x) C_ o -> ((F` A) e. o -> E.v e. L (F"v) C_ o)))
20	19	a1dd 53	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x e. ((nei` J)` {A}) -> ((F"x) C_ o -> (o C_ X -> ((F` A) e. o -> E.v e. L (F"v) C_ o))))
21	11, 20	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((J e. Top /\ x e. J /\ A e. x) -> ((F"x) C_ o -> (o C_ X -> ((F` A) e. o -> E.v e. L (F"v) C_ o))))
22	21	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (J e. Top -> (x e. J -> (A e. x -> ((F"x) C_ o -> (o C_ X -> ((F` A) e. o -> E.v e. L (F"v) C_ o))))))
23	22	3impd 1082	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (J e. Top -> ((x e. J /\ A e. x /\ (F"x) C_ o) -> (o C_ X -> ((F` A) e. o -> E.v e. L (F"v) C_ o))))
24	23	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((J e. Top /\ A e. Y) -> ((x e. J /\ A e. x /\ (F"x) C_ o) -> (o C_ X -> ((F` A) e. o -> E.v e. L (F"v) C_ o))))
25	24	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((o e. K /\ (J e. Top /\ K e. Top /\ A e. Y) /\ (J e. Top /\ A e. Y)) -> ((x e. J /\ A e. x /\ (F"x) C_ o) -> (o C_ X -> ((F` A) e. o -> E.v e. L (F"v) C_ o))))
26	25	com4l 43	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. J /\ A e. x /\ (F"x) C_ o) -> (o C_ X -> ((F` A) e. o -> ((o e. K /\ (J e. Top /\ K e. Top /\ A e. Y) /\ (J e. Top /\ A e. Y)) -> E.v e. L (F"v) C_ o))))
27	26	3expib 1070	. . . . . . . . . . . . . . . . . . . . . 22 |- (x e. J -> ((A e. x /\ (F"x) C_ o) -> (o C_ X -> ((F` A) e. o -> ((o e. K /\ (J e. Top /\ K e. Top /\ A e. Y) /\ (J e. Top /\ A e. Y)) -> E.v e. L (F"v) C_ o)))))
28	27	r19.23aiv 2211	. . . . . . . . . . . . . . . . . . . . 21 |- (E.x e. J (A e. x /\ (F"x) C_ o) -> (o C_ X -> ((F` A) e. o -> ((o e. K /\ (J e. Top /\ K e. Top /\ A e. Y) /\ (J e. Top /\ A e. Y)) -> E.v e. L (F"v) C_ o))))
29	28	com12 14	. . . . . . . . . . . . . . . . . . . 20 |- (o C_ X -> (E.x e. J (A e. x /\ (F"x) C_ o) -> ((F` A) e. o -> ((o e. K /\ (J e. Top /\ K e. Top /\ A e. Y) /\ (J e. Top /\ A e. Y)) -> E.v e. L (F"v) C_ o))))
30	29	com24 41	. . . . . . . . . . . . . . . . . . 19 |- (o C_ X -> ((o e. K /\ (J e. Top /\ K e. Top /\ A e. Y) /\ (J e. Top /\ A e. Y)) -> ((F` A) e. o -> (E.x e. J (A e. x /\ (F"x) C_ o) -> E.v e. L (F"v) C_ o))))
31	30	3expd 1085	. . . . . . . . . . . . . . . . . 18 |- (o C_ X -> (o e. K -> ((J e. Top /\ K e. Top /\ A e. Y) -> ((J e. Top /\ A e. Y) -> ((F` A) e. o -> (E.x e. J (A e. x /\ (F"x) C_ o) -> E.v e. L (F"v) C_ o))))))
32	10, 31	sylbi 216	. . . . . . . . . . . . . . . . 17 |- (o C_ U.K -> (o e. K -> ((J e. Top /\ K e. Top /\ A e. Y) -> ((J e. Top /\ A e. Y) -> ((F` A) e. o -> (E.x e. J (A e. x /\ (F"x) C_ o) -> E.v e. L (F"v) C_ o))))))
33	8, 32	mpcom 60	. . . . . . . . . . . . . . . 16 |- (o e. K -> ((J e. Top /\ K e. Top /\ A e. Y) -> ((J e. Top /\ A e. Y) -> ((F` A) e. o -> (E.x e. J (A e. x /\ (F"x) C_ o) -> E.v e. L (F"v) C_ o)))))
34	33	com13 37	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ A e. Y) -> ((J e. Top /\ K e. Top /\ A e. Y) -> (o e. K -> ((F` A) e. o -> (E.x e. J (A e. x /\ (F"x) C_ o) -> E.v e. L (F"v) C_ o)))))
35	34	3adant2 895	. . . . . . . . . . . . . 14 |- ((J e. Top /\ K e. Top /\ A e. Y) -> ((J e. Top /\ K e. Top /\ A e. Y) -> (o e. K -> ((F` A) e. o -> (E.x e. J (A e. x /\ (F"x) C_ o) -> E.v e. L (F"v) C_ o)))))
36	35	pm2.43i 78	. . . . . . . . . . . . 13 |- ((J e. Top /\ K e. Top /\ A e. Y) -> (o e. K -> ((F` A) e. o -> (E.x e. J (A e. x /\ (F"x) C_ o) -> E.v e. L (F"v) C_ o))))
37	36	imp31 389	. . . . . . . . . . . 12 |- ((((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) /\ (F` A) e. o) -> (E.x e. J (A e. x /\ (F"x) C_ o) -> E.v e. L (F"v) C_ o))
38	5	isneip 8996	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ A e. Y) -> (v e. ((nei` J)` {A}) <-> (v C_ Y /\ E.x e. J (A e. x /\ x C_ v))))
39		imass2 4299	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x C_ v -> (F"x) C_ (F"v))
40		sstr2 2623	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((F"x) C_ (F"v) -> ((F"v) C_ o -> (F"x) C_ o))
41	39, 40	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x C_ v -> ((F"v) C_ o -> (F"x) C_ o))
42	41	com12 14	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F"v) C_ o -> (x C_ v -> (F"x) C_ o))
43	42	anim2d 620	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F"v) C_ o -> ((A e. x /\ x C_ v) -> (A e. x /\ (F"x) C_ o)))
44	43	reximdv 2202	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F"v) C_ o -> (E.x e. J (A e. x /\ x C_ v) -> E.x e. J (A e. x /\ (F"x) C_ o)))
45	44	com12 14	. . . . . . . . . . . . . . . . . . . . 21 |- (E.x e. J (A e. x /\ x C_ v) -> ((F"v) C_ o -> E.x e. J (A e. x /\ (F"x) C_ o)))
46	45	a1d 15	. . . . . . . . . . . . . . . . . . . 20 |- (E.x e. J (A e. x /\ x C_ v) -> ((((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) /\ (F` A) e. o) -> ((F"v) C_ o -> E.x e. J (A e. x /\ (F"x) C_ o))))
47	46	adantl 424	. . . . . . . . . . . . . . . . . . 19 |- ((v C_ Y /\ E.x e. J (A e. x /\ x C_ v)) -> ((((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) /\ (F` A) e. o) -> ((F"v) C_ o -> E.x e. J (A e. x /\ (F"x) C_ o))))
48	38, 47	syl6bi 231	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ A e. Y) -> (v e. ((nei` J)` {A}) -> ((((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) /\ (F` A) e. o) -> ((F"v) C_ o -> E.x e. J (A e. x /\ (F"x) C_ o)))))
49	48	com23 36	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ A e. Y) -> ((((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) /\ (F` A) e. o) -> (v e. ((nei` J)` {A}) -> ((F"v) C_ o -> E.x e. J (A e. x /\ (F"x) C_ o)))))
50	49	3adant2 895	. . . . . . . . . . . . . . . 16 |- ((J e. Top /\ K e. Top /\ A e. Y) -> ((((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) /\ (F` A) e. o) -> (v e. ((nei` J)` {A}) -> ((F"v) C_ o -> E.x e. J (A e. x /\ (F"x) C_ o)))))
51	50	ad2antrr 440	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) /\ (F` A) e. o) -> ((((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) /\ (F` A) e. o) -> (v e. ((nei` J)` {A}) -> ((F"v) C_ o -> E.x e. J (A e. x /\ (F"x) C_ o)))))
52	51	pm2.43i 78	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) /\ (F` A) e. o) -> (v e. ((nei` J)` {A}) -> ((F"v) C_ o -> E.x e. J (A e. x /\ (F"x) C_ o))))
53	12	eleq2i 1961	. . . . . . . . . . . . . 14 |- (v e. L <-> v e. ((nei` J)` {A}))
54	52, 53	syl5ib 223	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) /\ (F` A) e. o) -> (v e. L -> ((F"v) C_ o -> E.x e. J (A e. x /\ (F"x) C_ o))))
55	54	r19.23adv 2215	. . . . . . . . . . . 12 |- ((((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) /\ (F` A) e. o) -> (E.v e. L (F"v) C_ o -> E.x e. J (A e. x /\ (F"x) C_ o)))
56	37, 55	impbid 574	. . . . . . . . . . 11 |- ((((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) /\ (F` A) e. o) -> (E.x e. J (A e. x /\ (F"x) C_ o) <-> E.v e. L (F"v) C_ o))
57	56	pm5.74da 646	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ A e. Y) /\ o e. K) -> (((F` A) e. o -> E.x e. J (A e. x /\ (F"x) C_ o)) <-> ((F` A) e. o -> E.v e. L (F"v) C_ o)))
58	57	ralbidva 2119	. . . . . . . . 9 |- ((J e. Top /\ K e. Top /\ A e. Y) -> (A.o e. K ((F` A) e. o -> E.x e. J (A e. x /\ (F"x) C_ o)) <-> A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o)))
59	58	anbi2d 678	. . . . . . . 8 |- ((J e. Top /\ K e. Top /\ A e. Y) -> ((F:Y-->X /\ A.o e. K ((F` A) e. o -> E.x e. J (A e. x /\ (F"x) C_ o))) <-> (F:Y-->X /\ A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o))))
60	7, 59	bitrd 587	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ A e. Y) -> (F e. ((J CnP K)` A) <-> (F:Y-->X /\ A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o))))
61	60	adantr 425	. . . . . 6 |- (((J e. Top /\ K e. Top /\ A e. Y) /\ F:Y-->X) -> (F e. ((J CnP K)` A) <-> (F:Y-->X /\ A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o))))
62		ibar 705	. . . . . . 7 |- (F:Y-->X -> (A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o) <-> (F:Y-->X /\ A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o))))
63	62	adantl 424	. . . . . 6 |- (((J e. Top /\ K e. Top /\ A e. Y) /\ F:Y-->X) -> (A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o) <-> (F:Y-->X /\ A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o))))
64	61, 63	bitr4d 590	. . . . 5 |- (((J e. Top /\ K e. Top /\ A e. Y) /\ F:Y-->X) -> (F e. ((J CnP K)` A) <-> A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o)))
65	64	3exp1 1084	. . . 4 |- (J e. Top -> (K e. Top -> (A e. Y -> (F:Y-->X -> (F e. ((J CnP K)` A) <-> A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o))))))
66	65	imp4a 391	. . 3 |- (J e. Top -> (K e. Top -> ((A e. Y /\ F:Y-->X) -> (F e. ((J CnP K)` A) <-> A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o)))))
67	66	3imp 1061	. 2 |- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> (F e. ((J CnP K)` A) <-> A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o)))
68		simp2 877	. . 3 |- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> K e. Top)
69		simp1 876	. . . . 5 |- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> J e. Top)
70		snssi 3129	. . . . . . 7 |- (A e. Y -> {A} C_ Y)
71	70	adantr 425	. . . . . 6 |- ((A e. Y /\ F:Y-->X) -> {A} C_ Y)
72	71	3ad2ant3 899	. . . . 5 |- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> {A} C_ Y)
73		snnzg 3118	. . . . . . 7 |- (A e. Y -> {A} =/= (/))
74	73	adantr 425	. . . . . 6 |- ((A e. Y /\ F:Y-->X) -> {A} =/= (/))
75	74	3ad2ant3 899	. . . . 5 |- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> {A} =/= (/))
76	5	neifil 10302	. . . . 5 |- ((J e. Top /\ {A} C_ Y /\ {A} =/= (/)) -> ((nei` J)` {A}) e. Fil)
77	69, 72, 75, 76	syl111anc 1100	. . . 4 |- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> ((nei` J)` {A}) e. Fil)
78	77, 12	syl5eqel 1975	. . 3 |- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> L e. Fil)
79	5	unnei 9011	. . . . . . . . . . . . . 14 |- ((J e. Top /\ {A} C_ Y) -> U.((nei` J)` {A}) = Y)
80	12	eqcomi 1888	. . . . . . . . . . . . . . 15 |- ((nei` J)` {A}) = L
81	80	unieqi 3187	. . . . . . . . . . . . . 14 |- U.((nei` J)` {A}) = U.L
82	79, 81	syl5reqr 1943	. . . . . . . . . . . . 13 |- ((J e. Top /\ {A} C_ Y) -> Y = U.L)
83	82	ex 402	. . . . . . . . . . . 12 |- (J e. Top -> ({A} C_ Y -> Y = U.L))
84	83	adantr 425	. . . . . . . . . . 11 |- ((J e. Top /\ K e. Top) -> ({A} C_ Y -> Y = U.L))
85	70, 84	mpan9 521	. . . . . . . . . 10 |- ((A e. Y /\ (J e. Top /\ K e. Top)) -> Y = U.L)
86	85	feq2d 4557	. . . . . . . . 9 |- ((A e. Y /\ (J e. Top /\ K e. Top)) -> (F:Y-->X <-> F:U.L-->X))
87	86	biimpd 170	. . . . . . . 8 |- ((A e. Y /\ (J e. Top /\ K e. Top)) -> (F:Y-->X -> F:U.L-->X))
88	87	ex 402	. . . . . . 7 |- (A e. Y -> ((J e. Top /\ K e. Top) -> (F:Y-->X -> F:U.L-->X)))
89	88	com23 36	. . . . . 6 |- (A e. Y -> (F:Y-->X -> ((J e. Top /\ K e. Top) -> F:U.L-->X)))
90	89	imp 377	. . . . 5 |- ((A e. Y /\ F:Y-->X) -> ((J e. Top /\ K e. Top) -> F:U.L-->X))
91	90	com12 14	. . . 4 |- ((J e. Top /\ K e. Top) -> ((A e. Y /\ F:Y-->X) -> F:U.L-->X))
92	91	3impia 1064	. . 3 |- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> F:U.L-->X)
93		eqid 1884	. . . 4 |- U.L = U.L
94	6, 93	isflimf 10323	. . 3 |- ((K e. Top /\ L e. Fil /\ F:U.L-->X) -> ((F` A) e. ((K fLimf L)` F) <-> ((F` A) e. X /\ A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o))))
95	68, 78, 92, 94	syl111anc 1100	. 2 |- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> ((F` A) e. ((K fLimf L)` F) <-> ((F` A) e. X /\ A.o e. K ((F` A) e. o -> E.v e. L (F"v) C_ o))))
96	4, 67, 95	3bitr4d 609	1 |- ((J e. Top /\ K e. Top /\ (A e. Y /\ F:Y-->X)) -> (F e. ((J CnP K)` A) <-> (F` A) e. ((K fLimf L)` F)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106   C_ wss 2593  (/)c0 2875  {csn 3044  U.cuni 3177  "cima 3989  -->wf 3994  ` cfv 3998  (class class class)co 4884  Topctop 8857  neicnei 8988   CnP ccnp 9029  Filcfil 10264   fLimf cflimf 10305

This theorem is referenced by:  conttnf2 14945

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  df-filmap 10306  df-flimf 10316

Copyright terms: Public domain