Theorem restcld 21484

Description: A closed set of a subspace topology is a closed set of the original topology intersected with the subset. (Contributed by FL, 11-Jul-2009.) (Proof shortened by Mario Carneiro, 15-Dec-2013.)

Hypothesis

Ref	Expression
restcld.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
restcld	⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘(𝐽 ↾t 𝑆)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐽   𝑥,𝑆   𝑥,𝑋

Proof of Theorem restcld

Dummy variable 𝑜 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 22	. . . . 5 ⊢ (𝑆 ⊆ 𝑋 → 𝑆 ⊆ 𝑋)
2		restcld.1	. . . . . 6 ⊢ 𝑋 = ∪ 𝐽
3	2	topopn 21218	. . . . 5 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
4		ssexg 5083	. . . . 5 ⊢ ((𝑆 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑆 ∈ V)
5	1, 3, 4	syl2anr 587	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ∈ V)
6		resttop 21472	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → (𝐽 ↾t 𝑆) ∈ Top)
7	5, 6	syldan 582	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐽 ↾t 𝑆) ∈ Top)
8		eqid 2779	. . . 4 ⊢ ∪ (𝐽 ↾t 𝑆) = ∪ (𝐽 ↾t 𝑆)
9	8	iscld 21339	. . 3 ⊢ ((𝐽 ↾t 𝑆) ∈ Top → (𝐴 ∈ (Clsd‘(𝐽 ↾t 𝑆)) ↔ (𝐴 ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (∪ (𝐽 ↾t 𝑆) ∖ 𝐴) ∈ (𝐽 ↾t 𝑆))))
10	7, 9	syl 17	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘(𝐽 ↾t 𝑆)) ↔ (𝐴 ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (∪ (𝐽 ↾t 𝑆) ∖ 𝐴) ∈ (𝐽 ↾t 𝑆))))
11	2	restuni 21474	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 = ∪ (𝐽 ↾t 𝑆))
12	11	sseq2d 3890	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐴 ⊆ 𝑆 ↔ 𝐴 ⊆ ∪ (𝐽 ↾t 𝑆)))
13	11	difeq1d 3989	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∖ 𝐴) = (∪ (𝐽 ↾t 𝑆) ∖ 𝐴))
14	13	eleq1d 2851	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆) ↔ (∪ (𝐽 ↾t 𝑆) ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)))
15	12, 14	anbi12d 621	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) ↔ (𝐴 ⊆ ∪ (𝐽 ↾t 𝑆) ∧ (∪ (𝐽 ↾t 𝑆) ∖ 𝐴) ∈ (𝐽 ↾t 𝑆))))
16		elrest 16557	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V) → ((𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)))
17	5, 16	syldan 582	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆) ↔ ∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)))
18	17	anbi2d 619	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) ↔ (𝐴 ⊆ 𝑆 ∧ ∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆))))
19	2	opncld 21345	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽) → (𝑋 ∖ 𝑜) ∈ (Clsd‘𝐽))
20	19	ad5ant14 745	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → (𝑋 ∖ 𝑜) ∈ (Clsd‘𝐽))
21		incom 4067	. . . . . . . . . . . 12 ⊢ (𝑋 ∩ 𝑆) = (𝑆 ∩ 𝑋)
22		df-ss 3844	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ 𝑋 ↔ (𝑆 ∩ 𝑋) = 𝑆)
23	22	biimpi 208	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ 𝑋 → (𝑆 ∩ 𝑋) = 𝑆)
24	21, 23	syl5eq 2827	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ 𝑋 → (𝑋 ∩ 𝑆) = 𝑆)
25	24	ad4antlr 720	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → (𝑋 ∩ 𝑆) = 𝑆)
26	25	difeq1d 3989	. . . . . . . . 9 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → ((𝑋 ∩ 𝑆) ∖ 𝑜) = (𝑆 ∖ 𝑜))
27		difeq2 3984	. . . . . . . . . . 11 ⊢ ((𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆) → (𝑆 ∖ (𝑆 ∖ 𝐴)) = (𝑆 ∖ (𝑜 ∩ 𝑆)))
28		difindi 4146	. . . . . . . . . . . 12 ⊢ (𝑆 ∖ (𝑜 ∩ 𝑆)) = ((𝑆 ∖ 𝑜) ∪ (𝑆 ∖ 𝑆))
29		difid 4217	. . . . . . . . . . . . 13 ⊢ (𝑆 ∖ 𝑆) = ∅
30	29	uneq2i 4026	. . . . . . . . . . . 12 ⊢ ((𝑆 ∖ 𝑜) ∪ (𝑆 ∖ 𝑆)) = ((𝑆 ∖ 𝑜) ∪ ∅)
31		un0 4231	. . . . . . . . . . . 12 ⊢ ((𝑆 ∖ 𝑜) ∪ ∅) = (𝑆 ∖ 𝑜)
32	28, 30, 31	3eqtri 2807	. . . . . . . . . . 11 ⊢ (𝑆 ∖ (𝑜 ∩ 𝑆)) = (𝑆 ∖ 𝑜)
33	27, 32	syl6eq 2831	. . . . . . . . . 10 ⊢ ((𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆) → (𝑆 ∖ (𝑆 ∖ 𝐴)) = (𝑆 ∖ 𝑜))
34	33	adantl 474	. . . . . . . . 9 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → (𝑆 ∖ (𝑆 ∖ 𝐴)) = (𝑆 ∖ 𝑜))
35		dfss4 4123	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝑆 ↔ (𝑆 ∖ (𝑆 ∖ 𝐴)) = 𝐴)
36	35	biimpi 208	. . . . . . . . . 10 ⊢ (𝐴 ⊆ 𝑆 → (𝑆 ∖ (𝑆 ∖ 𝐴)) = 𝐴)
37	36	ad3antlr 718	. . . . . . . . 9 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → (𝑆 ∖ (𝑆 ∖ 𝐴)) = 𝐴)
38	26, 34, 37	3eqtr2rd 2822	. . . . . . . 8 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → 𝐴 = ((𝑋 ∩ 𝑆) ∖ 𝑜))
39	21	difeq1i 3986	. . . . . . . . 9 ⊢ ((𝑋 ∩ 𝑆) ∖ 𝑜) = ((𝑆 ∩ 𝑋) ∖ 𝑜)
40		indif2 4135	. . . . . . . . 9 ⊢ (𝑆 ∩ (𝑋 ∖ 𝑜)) = ((𝑆 ∩ 𝑋) ∖ 𝑜)
41		incom 4067	. . . . . . . . 9 ⊢ (𝑆 ∩ (𝑋 ∖ 𝑜)) = ((𝑋 ∖ 𝑜) ∩ 𝑆)
42	39, 40, 41	3eqtr2i 2809	. . . . . . . 8 ⊢ ((𝑋 ∩ 𝑆) ∖ 𝑜) = ((𝑋 ∖ 𝑜) ∩ 𝑆)
43	38, 42	syl6eq 2831	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → 𝐴 = ((𝑋 ∖ 𝑜) ∩ 𝑆))
44		ineq1 4069	. . . . . . . 8 ⊢ (𝑥 = (𝑋 ∖ 𝑜) → (𝑥 ∩ 𝑆) = ((𝑋 ∖ 𝑜) ∩ 𝑆))
45	44	rspceeqv 3554	. . . . . . 7 ⊢ (((𝑋 ∖ 𝑜) ∈ (Clsd‘𝐽) ∧ 𝐴 = ((𝑋 ∖ 𝑜) ∩ 𝑆)) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))
46	20, 43, 45	syl2anc 576	. . . . . 6 ⊢ (((((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) ∧ 𝑜 ∈ 𝐽) ∧ (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))
47	46	rexlimdva2 3233	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴 ⊆ 𝑆) → (∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆)))
48	47	expimpd 446	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ ∃𝑜 ∈ 𝐽 (𝑆 ∖ 𝐴) = (𝑜 ∩ 𝑆)) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆)))
49	18, 48	sylbid 232	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) → ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆)))
50		difindi 4146	. . . . . . . . . 10 ⊢ (𝑆 ∖ (𝑥 ∩ 𝑆)) = ((𝑆 ∖ 𝑥) ∪ (𝑆 ∖ 𝑆))
51	29	uneq2i 4026	. . . . . . . . . 10 ⊢ ((𝑆 ∖ 𝑥) ∪ (𝑆 ∖ 𝑆)) = ((𝑆 ∖ 𝑥) ∪ ∅)
52		un0 4231	. . . . . . . . . 10 ⊢ ((𝑆 ∖ 𝑥) ∪ ∅) = (𝑆 ∖ 𝑥)
53	50, 51, 52	3eqtri 2807	. . . . . . . . 9 ⊢ (𝑆 ∖ (𝑥 ∩ 𝑆)) = (𝑆 ∖ 𝑥)
54		difin2 4154	. . . . . . . . . 10 ⊢ (𝑆 ⊆ 𝑋 → (𝑆 ∖ 𝑥) = ((𝑋 ∖ 𝑥) ∩ 𝑆))
55	54	adantl 474	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∖ 𝑥) = ((𝑋 ∖ 𝑥) ∩ 𝑆))
56	53, 55	syl5eq 2827	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∖ (𝑥 ∩ 𝑆)) = ((𝑋 ∖ 𝑥) ∩ 𝑆))
57	56	adantr 473	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑆 ∖ (𝑥 ∩ 𝑆)) = ((𝑋 ∖ 𝑥) ∩ 𝑆))
58		simpll 754	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝐽 ∈ Top)
59	5	adantr 473	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑆 ∈ V)
60	2	cldopn 21343	. . . . . . . . 9 ⊢ (𝑥 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑥) ∈ 𝐽)
61	60	adantl 474	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑥) ∈ 𝐽)
62		elrestr 16558	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ V ∧ (𝑋 ∖ 𝑥) ∈ 𝐽) → ((𝑋 ∖ 𝑥) ∩ 𝑆) ∈ (𝐽 ↾t 𝑆))
63	58, 59, 61, 62	syl3anc 1351	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑋 ∖ 𝑥) ∩ 𝑆) ∈ (𝐽 ↾t 𝑆))
64	57, 63	eqeltrd 2867	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑆 ∖ (𝑥 ∩ 𝑆)) ∈ (𝐽 ↾t 𝑆))
65		inss2 4094	. . . . . 6 ⊢ (𝑥 ∩ 𝑆) ⊆ 𝑆
66	64, 65	jctil 512	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 ∩ 𝑆) ⊆ 𝑆 ∧ (𝑆 ∖ (𝑥 ∩ 𝑆)) ∈ (𝐽 ↾t 𝑆)))
67		sseq1 3883	. . . . . 6 ⊢ (𝐴 = (𝑥 ∩ 𝑆) → (𝐴 ⊆ 𝑆 ↔ (𝑥 ∩ 𝑆) ⊆ 𝑆))
68		difeq2 3984	. . . . . . 7 ⊢ (𝐴 = (𝑥 ∩ 𝑆) → (𝑆 ∖ 𝐴) = (𝑆 ∖ (𝑥 ∩ 𝑆)))
69	68	eleq1d 2851	. . . . . 6 ⊢ (𝐴 = (𝑥 ∩ 𝑆) → ((𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆) ↔ (𝑆 ∖ (𝑥 ∩ 𝑆)) ∈ (𝐽 ↾t 𝑆)))
70	67, 69	anbi12d 621	. . . . 5 ⊢ (𝐴 = (𝑥 ∩ 𝑆) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) ↔ ((𝑥 ∩ 𝑆) ⊆ 𝑆 ∧ (𝑆 ∖ (𝑥 ∩ 𝑆)) ∈ (𝐽 ↾t 𝑆))))
71	66, 70	syl5ibrcom 239	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝐴 = (𝑥 ∩ 𝑆) → (𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆))))
72	71	rexlimdva 3230	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆) → (𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆))))
73	49, 72	impbid 204	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐴 ⊆ 𝑆 ∧ (𝑆 ∖ 𝐴) ∈ (𝐽 ↾t 𝑆)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆)))
74	10, 15, 73	3bitr2d 299	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘(𝐽 ↾t 𝑆)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆)))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507   ∈ wcel 2050  ∃wrex 3090  Vcvv 3416   ∖ cdif 3827   ∪ cun 3828   ∩ cin 3829   ⊆ wss 3830  ∅c0 4179  ∪ cuni 4712  ‘cfv 6188  (class class class)co 6976   ↾_t crest 16550  Topctop 21205  Clsdccld 21328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ne 2969  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-pss 3846  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-ov 6979  df-oprab 6980  df-mpo 6981  df-om 7397  df-1st 7501  df-2nd 7502  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-oadd 7909  df-er 8089  df-en 8307  df-fin 8310  df-fi 8670  df-rest 16552  df-topgen 16573  df-top 21206  df-topon 21223  df-bases 21258  df-cld 21331

This theorem is referenced by:  restcldi  21485  restcldr  21486  restcls  21493  connsubclo  21736  cldllycmp  21807