Description: The set of singletons is locally finite in the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | dissnref.c | |
|
Assertion | dissnlocfin | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dissnref.c | |
|
2 | distop | |
|
3 | eqidd | |
|
4 | snelpwi | |
|
5 | 4 | adantl | |
6 | vsnid | |
|
7 | 6 | a1i | |
8 | nfv | |
|
9 | nfrab1 | |
|
10 | nfcv | |
|
11 | 1 | abeq2i | |
12 | 11 | anbi1i | |
13 | simpr | |
|
14 | simplr | |
|
15 | 14 | ineq1d | |
16 | disjsn2 | |
|
17 | 16 | adantl | |
18 | 15 17 | eqtrd | |
19 | simp-4r | |
|
20 | 19 | neneqd | |
21 | 18 20 | pm2.65da | |
22 | nne | |
|
23 | 21 22 | sylib | |
24 | 23 | sneqd | |
25 | 13 24 | eqtrd | |
26 | 25 | r19.29an | |
27 | 26 | an32s | |
28 | 27 | anasss | |
29 | sneq | |
|
30 | 29 | rspceeqv | |
31 | 30 | adantll | |
32 | simpr | |
|
33 | 32 | ineq1d | |
34 | inidm | |
|
35 | 33 34 | eqtrdi | |
36 | vex | |
|
37 | 36 | snnz | |
38 | 37 | a1i | |
39 | 35 38 | eqnetrd | |
40 | 31 39 | jca | |
41 | 28 40 | impbida | |
42 | 12 41 | syl5bb | |
43 | rabid | |
|
44 | velsn | |
|
45 | 42 43 44 | 3bitr4g | |
46 | 8 9 10 45 | eqrd | |
47 | snfi | |
|
48 | 46 47 | eqeltrdi | |
49 | eleq2 | |
|
50 | ineq2 | |
|
51 | 50 | neeq1d | |
52 | 51 | rabbidv | |
53 | 52 | eleq1d | |
54 | 49 53 | anbi12d | |
55 | 54 | rspcev | |
56 | 5 7 48 55 | syl12anc | |
57 | 56 | ralrimiva | |
58 | unipw | |
|
59 | 58 | eqcomi | |
60 | 1 | unisngl | |
61 | 59 60 | islocfin | |
62 | 2 3 57 61 | syl3anbrc | |