Description: A normal R_0 space is also regular. These spaces are usually referred to as normal regular spaces. (Contributed by Mario Carneiro, 25-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | nrmr0reg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nrmtop | |
|
2 | 1 | adantr | |
3 | simpll | |
|
4 | simprl | |
|
5 | 2 | adantr | |
6 | toptopon2 | |
|
7 | 5 6 | sylib | |
8 | simplr | |
|
9 | simprr | |
|
10 | elunii | |
|
11 | 9 4 10 | syl2anc | |
12 | eqid | |
|
13 | 12 | r0cld | |
14 | 7 8 11 13 | syl3anc | |
15 | simp1rr | |
|
16 | 4 | adantr | |
17 | elequ2 | |
|
18 | elequ2 | |
|
19 | 17 18 | bibi12d | |
20 | 19 | rspcv | |
21 | 16 20 | syl | |
22 | 21 | 3impia | |
23 | 15 22 | mpbird | |
24 | 23 | rabssdv | |
25 | nrmsep3 | |
|
26 | 3 4 14 24 25 | syl13anc | |
27 | elequ1 | |
|
28 | 27 | bibi1d | |
29 | 28 | ralbidv | |
30 | biidd | |
|
31 | 30 | ralrimivw | |
32 | 29 11 31 | elrabd | |
33 | ssel | |
|
34 | 32 33 | syl5com | |
35 | 34 | anim1d | |
36 | 35 | reximdv | |
37 | 26 36 | mpd | |
38 | 37 | ralrimivva | |
39 | isreg | |
|
40 | 2 38 39 | sylanbrc | |