Theorem paste 15893

Description: Pasting lemma. If A and B are closed sets in X with A u. B = X, then any function whose restrictions to A and B are continuous is continuous on all of X.

Hypotheses

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

Assertion

Ref	Expression
paste	|- (((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> F e. (J Cn K))

Proof of Theorem paste

Step	Hyp	Ref	Expression
1		paste.1	. . . 4 |- X = U.J
2		paste.2	. . . 4 |- Y = U.K
3	1, 2	iscncl 9047	. . 3 |- ((J e. Top /\ K e. Top) -> (F e. (J Cn K) <-> (F:X-->Y /\ A.y e. (Clsd` K)(`'F"y) e. (Clsd` J))))
4	3	3ad2ant1 897	. 2 |- (((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> (F e. (J Cn K) <-> (F:X-->Y /\ A.y e. (Clsd` K)(`'F"y) e. (Clsd` J))))
5		simp1 876	. . 3 |- ((F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K)) -> F:X-->Y)
6	5	3ad2ant3 899	. 2 |- (((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> F:X-->Y)
7		imassrn 4278	. . . . . . . . . . . . 13 |- (`'F"y) C_ ran `' F
8	7	a1i 8	. . . . . . . . . . . 12 |- (F:X-->Y -> (`'F"y) C_ ran `' F)
9		fdm 4567	. . . . . . . . . . . . 13 |- (F:X-->Y -> dom F = X)
10		dfdm4 4151	. . . . . . . . . . . . 13 |- dom F = ran `' F
11	9, 10	syl5eqr 1942	. . . . . . . . . . . 12 |- (F:X-->Y -> ran `' F = X)
12	8, 11	sseqtrd 2653	. . . . . . . . . . 11 |- (F:X-->Y -> (`'F"y) C_ X)
13		df-ss 2605	. . . . . . . . . . . . 13 |- ((`'F"y) C_ X <-> ((`'F"y) i^i X) = (`'F"y))
14	13	biimpi 168	. . . . . . . . . . . 12 |- ((`'F"y) C_ X -> ((`'F"y) i^i X) = (`'F"y))
15	14	eqcomd 1889	. . . . . . . . . . 11 |- ((`'F"y) C_ X -> (`'F"y) = ((`'F"y) i^i X))
16	12, 15	syl 12	. . . . . . . . . 10 |- (F:X-->Y -> (`'F"y) = ((`'F"y) i^i X))
17	16	adantl 424	. . . . . . . . 9 |- (((A u. B) = X /\ F:X-->Y) -> (`'F"y) = ((`'F"y) i^i X))
18		ineq2 2790	. . . . . . . . . . 11 |- (X = (A u. B) -> ((`'F"y) i^i X) = ((`'F"y) i^i (A u. B)))
19	18	eqcoms 1887	. . . . . . . . . 10 |- ((A u. B) = X -> ((`'F"y) i^i X) = ((`'F"y) i^i (A u. B)))
20	19	adantr 425	. . . . . . . . 9 |- (((A u. B) = X /\ F:X-->Y) -> ((`'F"y) i^i X) = ((`'F"y) i^i (A u. B)))
21		ffun 4565	. . . . . . . . . . . 12 |- (F:X-->Y -> Fun F)
22		respreima 15684	. . . . . . . . . . . . 13 |- (Fun F -> (`'(F |` A)"y) = ((`'F"y) i^i A))
23		respreima 15684	. . . . . . . . . . . . 13 |- (Fun F -> (`'(F |` B)"y) = ((`'F"y) i^i B))
24	22, 23	uneq12d 2756	. . . . . . . . . . . 12 |- (Fun F -> ((`'(F |` A)"y) u. (`'(F |` B)"y)) = (((`'F"y) i^i A) u. ((`'F"y) i^i B)))
25	21, 24	syl 12	. . . . . . . . . . 11 |- (F:X-->Y -> ((`'(F |` A)"y) u. (`'(F |` B)"y)) = (((`'F"y) i^i A) u. ((`'F"y) i^i B)))
26		indi 2838	. . . . . . . . . . 11 |- ((`'F"y) i^i (A u. B)) = (((`'F"y) i^i A) u. ((`'F"y) i^i B))
27	25, 26	syl6reqr 1947	. . . . . . . . . 10 |- (F:X-->Y -> ((`'F"y) i^i (A u. B)) = ((`'(F |` A)"y) u. (`'(F |` B)"y)))
28	27	adantl 424	. . . . . . . . 9 |- (((A u. B) = X /\ F:X-->Y) -> ((`'F"y) i^i (A u. B)) = ((`'(F |` A)"y) u. (`'(F |` B)"y)))
29	17, 20, 28	3eqtrd 1929	. . . . . . . 8 |- (((A u. B) = X /\ F:X-->Y) -> (`'F"y) = ((`'(F |` A)"y) u. (`'(F |` B)"y)))
30	29	3ad2antr1 1041	. . . . . . 7 |- (((A u. B) = X /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> (`'F"y) = ((`'(F |` A)"y) u. (`'(F |` B)"y)))
31	30	3ad2antl3 1040	. . . . . 6 |- (((A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> (`'F"y) = ((`'(F |` A)"y) u. (`'(F |` B)"y)))
32	31	3adant1 894	. . . . 5 |- (((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> (`'F"y) = ((`'(F |` A)"y) u. (`'(F |` B)"y)))
33	32	adantr 425	. . . 4 |- ((((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) /\ y e. (Clsd` K)) -> (`'F"y) = ((`'(F |` A)"y) u. (`'(F |` B)"y)))
34		simpl1l 927	. . . . 5 |- ((((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) /\ y e. (Clsd` K)) -> J e. Top)
35		cnclima 9048	. . . . . . . . . . . . . . . 16 |- ((((subSp` <.A, J>.) e. Top /\ K e. Top /\ (F |` A) e. ((subSp` <.A, J>.) Cn K)) /\ y e. (Clsd` K)) -> (`'(F |` A)"y) e. (Clsd` (subSp` <.A, J>.)))
36	35	ex 402	. . . . . . . . . . . . . . 15 |- (((subSp` <.A, J>.) e. Top /\ K e. Top /\ (F |` A) e. ((subSp` <.A, J>.) Cn K)) -> (y e. (Clsd` K) -> (`'(F |` A)"y) e. (Clsd` (subSp` <.A, J>.))))
37	36	3expia 1069	. . . . . . . . . . . . . 14 |- (((subSp` <.A, J>.) e. Top /\ K e. Top) -> ((F |` A) e. ((subSp` <.A, J>.) Cn K) -> (y e. (Clsd` K) -> (`'(F |` A)"y) e. (Clsd` (subSp` <.A, J>.)))))
38		eqid 1884	. . . . . . . . . . . . . . . 16 |- U.J = U.J
39	38	cldss 8947	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ A e. (Clsd` J)) -> A C_ U.J)
40		stoig3 10253	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ A C_ U.J) -> (subSp` <.A, J>.) e. Top)
41	39, 40	syldan 516	. . . . . . . . . . . . . 14 |- ((J e. Top /\ A e. (Clsd` J)) -> (subSp` <.A, J>.) e. Top)
42	37, 41	sylan 497	. . . . . . . . . . . . 13 |- (((J e. Top /\ A e. (Clsd` J)) /\ K e. Top) -> ((F |` A) e. ((subSp` <.A, J>.) Cn K) -> (y e. (Clsd` K) -> (`'(F |` A)"y) e. (Clsd` (subSp` <.A, J>.)))))
43	42	an1rs 547	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top) /\ A e. (Clsd` J)) -> ((F |` A) e. ((subSp` <.A, J>.) Cn K) -> (y e. (Clsd` K) -> (`'(F |` A)"y) e. (Clsd` (subSp` <.A, J>.)))))
44	43	imp 377	. . . . . . . . . . 11 |- ((((J e. Top /\ K e. Top) /\ A e. (Clsd` J)) /\ (F |` A) e. ((subSp` <.A, J>.) Cn K)) -> (y e. (Clsd` K) -> (`'(F |` A)"y) e. (Clsd` (subSp` <.A, J>.))))
45		subspcld2 15839	. . . . . . . . . . . . . 14 |- ((J e. Top /\ A e. (Clsd` J) /\ (`'(F |` A)"y) e. (Clsd` (subSp` <.A, J>.))) -> (`'(F |` A)"y) e. (Clsd` J))
46	45	3expia 1069	. . . . . . . . . . . . 13 |- ((J e. Top /\ A e. (Clsd` J)) -> ((`'(F |` A)"y) e. (Clsd` (subSp` <.A, J>.)) -> (`'(F |` A)"y) e. (Clsd` J)))
47	46	adantlr 429	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top) /\ A e. (Clsd` J)) -> ((`'(F |` A)"y) e. (Clsd` (subSp` <.A, J>.)) -> (`'(F |` A)"y) e. (Clsd` J)))
48	47	adantr 425	. . . . . . . . . . 11 |- ((((J e. Top /\ K e. Top) /\ A e. (Clsd` J)) /\ (F |` A) e. ((subSp` <.A, J>.) Cn K)) -> ((`'(F |` A)"y) e. (Clsd` (subSp` <.A, J>.)) -> (`'(F |` A)"y) e. (Clsd` J)))
49	44, 48	syld 30	. . . . . . . . . 10 |- ((((J e. Top /\ K e. Top) /\ A e. (Clsd` J)) /\ (F |` A) e. ((subSp` <.A, J>.) Cn K)) -> (y e. (Clsd` K) -> (`'(F |` A)"y) e. (Clsd` J)))
50	49	3ad2antr2 1042	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top) /\ A e. (Clsd` J)) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> (y e. (Clsd` K) -> (`'(F |` A)"y) e. (Clsd` J)))
51	50	ex 402	. . . . . . . 8 |- (((J e. Top /\ K e. Top) /\ A e. (Clsd` J)) -> ((F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K)) -> (y e. (Clsd` K) -> (`'(F |` A)"y) e. (Clsd` J))))
52	51	3ad2antr1 1041	. . . . . . 7 |- (((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X)) -> ((F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K)) -> (y e. (Clsd` K) -> (`'(F |` A)"y) e. (Clsd` J))))
53	52	3impia 1064	. . . . . 6 |- (((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> (y e. (Clsd` K) -> (`'(F |` A)"y) e. (Clsd` J)))
54	53	imp 377	. . . . 5 |- ((((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) /\ y e. (Clsd` K)) -> (`'(F |` A)"y) e. (Clsd` J))
55		cnclima 9048	. . . . . . . . . . . . . . . 16 |- ((((subSp` <.B, J>.) e. Top /\ K e. Top /\ (F |` B) e. ((subSp` <.B, J>.) Cn K)) /\ y e. (Clsd` K)) -> (`'(F |` B)"y) e. (Clsd` (subSp` <.B, J>.)))
56	55	ex 402	. . . . . . . . . . . . . . 15 |- (((subSp` <.B, J>.) e. Top /\ K e. Top /\ (F |` B) e. ((subSp` <.B, J>.) Cn K)) -> (y e. (Clsd` K) -> (`'(F |` B)"y) e. (Clsd` (subSp` <.B, J>.))))
57	56	3expia 1069	. . . . . . . . . . . . . 14 |- (((subSp` <.B, J>.) e. Top /\ K e. Top) -> ((F |` B) e. ((subSp` <.B, J>.) Cn K) -> (y e. (Clsd` K) -> (`'(F |` B)"y) e. (Clsd` (subSp` <.B, J>.)))))
58	38	cldss 8947	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ B e. (Clsd` J)) -> B C_ U.J)
59		stoig3 10253	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ B C_ U.J) -> (subSp` <.B, J>.) e. Top)
60	58, 59	syldan 516	. . . . . . . . . . . . . 14 |- ((J e. Top /\ B e. (Clsd` J)) -> (subSp` <.B, J>.) e. Top)
61	57, 60	sylan 497	. . . . . . . . . . . . 13 |- (((J e. Top /\ B e. (Clsd` J)) /\ K e. Top) -> ((F |` B) e. ((subSp` <.B, J>.) Cn K) -> (y e. (Clsd` K) -> (`'(F |` B)"y) e. (Clsd` (subSp` <.B, J>.)))))
62	61	an1rs 547	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top) /\ B e. (Clsd` J)) -> ((F |` B) e. ((subSp` <.B, J>.) Cn K) -> (y e. (Clsd` K) -> (`'(F |` B)"y) e. (Clsd` (subSp` <.B, J>.)))))
63	62	imp 377	. . . . . . . . . . 11 |- ((((J e. Top /\ K e. Top) /\ B e. (Clsd` J)) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K)) -> (y e. (Clsd` K) -> (`'(F |` B)"y) e. (Clsd` (subSp` <.B, J>.))))
64		subspcld2 15839	. . . . . . . . . . . . . 14 |- ((J e. Top /\ B e. (Clsd` J) /\ (`'(F |` B)"y) e. (Clsd` (subSp` <.B, J>.))) -> (`'(F |` B)"y) e. (Clsd` J))
65	64	3expia 1069	. . . . . . . . . . . . 13 |- ((J e. Top /\ B e. (Clsd` J)) -> ((`'(F |` B)"y) e. (Clsd` (subSp` <.B, J>.)) -> (`'(F |` B)"y) e. (Clsd` J)))
66	65	adantlr 429	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top) /\ B e. (Clsd` J)) -> ((`'(F |` B)"y) e. (Clsd` (subSp` <.B, J>.)) -> (`'(F |` B)"y) e. (Clsd` J)))
67	66	adantr 425	. . . . . . . . . . 11 |- ((((J e. Top /\ K e. Top) /\ B e. (Clsd` J)) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K)) -> ((`'(F |` B)"y) e. (Clsd` (subSp` <.B, J>.)) -> (`'(F |` B)"y) e. (Clsd` J)))
68	63, 67	syld 30	. . . . . . . . . 10 |- ((((J e. Top /\ K e. Top) /\ B e. (Clsd` J)) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K)) -> (y e. (Clsd` K) -> (`'(F |` B)"y) e. (Clsd` J)))
69	68	3ad2antr3 1043	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top) /\ B e. (Clsd` J)) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> (y e. (Clsd` K) -> (`'(F |` B)"y) e. (Clsd` J)))
70	69	ex 402	. . . . . . . 8 |- (((J e. Top /\ K e. Top) /\ B e. (Clsd` J)) -> ((F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K)) -> (y e. (Clsd` K) -> (`'(F |` B)"y) e. (Clsd` J))))
71	70	3ad2antr2 1042	. . . . . . 7 |- (((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X)) -> ((F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K)) -> (y e. (Clsd` K) -> (`'(F |` B)"y) e. (Clsd` J))))
72	71	3impia 1064	. . . . . 6 |- (((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> (y e. (Clsd` K) -> (`'(F |` B)"y) e. (Clsd` J)))
73	72	imp 377	. . . . 5 |- ((((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) /\ y e. (Clsd` K)) -> (`'(F |` B)"y) e. (Clsd` J))
74		uncld 8957	. . . . 5 |- ((J e. Top /\ (`'(F |` A)"y) e. (Clsd` J) /\ (`'(F |` B)"y) e. (Clsd` J)) -> ((`'(F |` A)"y) u. (`'(F |` B)"y)) e. (Clsd` J))
75	34, 54, 73, 74	syl111anc 1100	. . . 4 |- ((((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) /\ y e. (Clsd` K)) -> ((`'(F |` A)"y) u. (`'(F |` B)"y)) e. (Clsd` J))
76	33, 75	eqeltrd 1971	. . 3 |- ((((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) /\ y e. (Clsd` K)) -> (`'F"y) e. (Clsd` J))
77	76	r19.21aiva 2176	. 2 |- (((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> A.y e. (Clsd` K)(`'F"y) e. (Clsd` J))
78	4, 6, 77	mpbir2and 802	1 |- (((J e. Top /\ K e. Top) /\ (A e. (Clsd` J) /\ B e. (Clsd` J) /\ (A u. B) = X) /\ (F:X-->Y /\ (F |` A) e. ((subSp` <.A, J>.) Cn K) /\ (F |` B) e. ((subSp` <.B, J>.) Cn K))) -> F e. (J Cn K))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105   u. cun 2591   i^i cin 2592   C_ wss 2593  <.cop 3046  U.cuni 3177  `'ccnv 3985  dom cdm 3986  ran crn 3987   |` cres 3988  "cima 3989  Fun wfun 3992  -->wf 3994  ` cfv 3998  (class class class)co 4884  Topctop 8857  Clsdccld 8936   Cn ccn 9028  subSpcsubsp 10242

This theorem is referenced by:  piececn 15894  phtpycolem5 16055  pcocn 16076  pcohtpylem3 16082  pcorevlem 16086

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  ax-reg 5695

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-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  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-topsp 8862  df-cld 8939  df-cn 9030  df-subsp 10243

Copyright terms: Public domain