Metamath Proof Explorer


Theorem nrmr0reg

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 JNrmKQJFreJReg

Proof

Step Hyp Ref Expression
1 nrmtop JNrmJTop
2 1 adantr JNrmKQJFreJTop
3 simpll JNrmKQJFrexJyxJNrm
4 simprl JNrmKQJFrexJyxxJ
5 2 adantr JNrmKQJFrexJyxJTop
6 toptopon2 JTopJTopOnJ
7 5 6 sylib JNrmKQJFrexJyxJTopOnJ
8 simplr JNrmKQJFrexJyxKQJFre
9 simprr JNrmKQJFrexJyxyx
10 elunii yxxJyJ
11 9 4 10 syl2anc JNrmKQJFrexJyxyJ
12 eqid zJwJ|zw=zJwJ|zw
13 12 r0cld JTopOnJKQJFreyJaJ|bJabybClsdJ
14 7 8 11 13 syl3anc JNrmKQJFrexJyxaJ|bJabybClsdJ
15 simp1rr JNrmKQJFrexJyxaJbJabybyx
16 4 adantr JNrmKQJFrexJyxaJxJ
17 elequ2 b=xabax
18 elequ2 b=xybyx
19 17 18 bibi12d b=xabybaxyx
20 19 rspcv xJbJabybaxyx
21 16 20 syl JNrmKQJFrexJyxaJbJabybaxyx
22 21 3impia JNrmKQJFrexJyxaJbJabybaxyx
23 15 22 mpbird JNrmKQJFrexJyxaJbJabybax
24 23 rabssdv JNrmKQJFrexJyxaJ|bJabybx
25 nrmsep3 JNrmxJaJ|bJabybClsdJaJ|bJabybxzJaJ|bJabybzclsJzx
26 3 4 14 24 25 syl13anc JNrmKQJFrexJyxzJaJ|bJabybzclsJzx
27 elequ1 a=yabyb
28 27 bibi1d a=yabybybyb
29 28 ralbidv a=ybJabybbJybyb
30 biidd JNrmKQJFrexJyxybyb
31 30 ralrimivw JNrmKQJFrexJyxbJybyb
32 29 11 31 elrabd JNrmKQJFrexJyxyaJ|bJabyb
33 ssel aJ|bJabybzyaJ|bJabybyz
34 32 33 syl5com JNrmKQJFrexJyxaJ|bJabybzyz
35 34 anim1d JNrmKQJFrexJyxaJ|bJabybzclsJzxyzclsJzx
36 35 reximdv JNrmKQJFrexJyxzJaJ|bJabybzclsJzxzJyzclsJzx
37 26 36 mpd JNrmKQJFrexJyxzJyzclsJzx
38 37 ralrimivva JNrmKQJFrexJyxzJyzclsJzx
39 isreg JRegJTopxJyxzJyzclsJzx
40 2 38 39 sylanbrc JNrmKQJFreJReg