Metamath Proof Explorer

Theorem isreg2

Description: A topological space is regular if any closed set is separated from any point not in it by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion isreg2 ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left({J}\in \mathrm{Reg}↔\forall {c}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)$

Proof

Step Hyp Ref Expression
1 simp1r ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Reg}\right)\wedge \left({c}\in \mathrm{Clsd}\left({J}\right)\wedge {x}\in {X}\right)\wedge ¬{x}\in {c}\right)\to {J}\in \mathrm{Reg}$
2 simp2l ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Reg}\right)\wedge \left({c}\in \mathrm{Clsd}\left({J}\right)\wedge {x}\in {X}\right)\wedge ¬{x}\in {c}\right)\to {c}\in \mathrm{Clsd}\left({J}\right)$
3 simp2r ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Reg}\right)\wedge \left({c}\in \mathrm{Clsd}\left({J}\right)\wedge {x}\in {X}\right)\wedge ¬{x}\in {c}\right)\to {x}\in {X}$
4 simp1l ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Reg}\right)\wedge \left({c}\in \mathrm{Clsd}\left({J}\right)\wedge {x}\in {X}\right)\wedge ¬{x}\in {c}\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
5 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}=\bigcup {J}$
6 4 5 syl ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Reg}\right)\wedge \left({c}\in \mathrm{Clsd}\left({J}\right)\wedge {x}\in {X}\right)\wedge ¬{x}\in {c}\right)\to {X}=\bigcup {J}$
7 3 6 eleqtrd ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Reg}\right)\wedge \left({c}\in \mathrm{Clsd}\left({J}\right)\wedge {x}\in {X}\right)\wedge ¬{x}\in {c}\right)\to {x}\in \bigcup {J}$
8 simp3 ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Reg}\right)\wedge \left({c}\in \mathrm{Clsd}\left({J}\right)\wedge {x}\in {X}\right)\wedge ¬{x}\in {c}\right)\to ¬{x}\in {c}$
9 eqid ${⊢}\bigcup {J}=\bigcup {J}$
10 9 regsep2 ${⊢}\left({J}\in \mathrm{Reg}\wedge \left({c}\in \mathrm{Clsd}\left({J}\right)\wedge {x}\in \bigcup {J}\wedge ¬{x}\in {c}\right)\right)\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)$
11 1 2 7 8 10 syl13anc ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Reg}\right)\wedge \left({c}\in \mathrm{Clsd}\left({J}\right)\wedge {x}\in {X}\right)\wedge ¬{x}\in {c}\right)\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)$
12 11 3expia ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Reg}\right)\wedge \left({c}\in \mathrm{Clsd}\left({J}\right)\wedge {x}\in {X}\right)\right)\to \left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)$
13 12 ralrimivva ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\in \mathrm{Reg}\right)\to \forall {c}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)$
14 topontop ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {J}\in \mathrm{Top}$
15 14 adantr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \forall {c}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {J}\in \mathrm{Top}$
16 5 adantr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\to {X}=\bigcup {J}$
17 16 difeq1d ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\to {X}\setminus {y}=\bigcup {J}\setminus {y}$
18 9 opncld ${⊢}\left({J}\in \mathrm{Top}\wedge {y}\in {J}\right)\to \bigcup {J}\setminus {y}\in \mathrm{Clsd}\left({J}\right)$
19 14 18 sylan ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\to \bigcup {J}\setminus {y}\in \mathrm{Clsd}\left({J}\right)$
20 17 19 eqeltrd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\to {X}\setminus {y}\in \mathrm{Clsd}\left({J}\right)$
21 eleq2 ${⊢}{c}={X}\setminus {y}\to \left({x}\in {c}↔{x}\in \left({X}\setminus {y}\right)\right)$
22 21 notbid ${⊢}{c}={X}\setminus {y}\to \left(¬{x}\in {c}↔¬{x}\in \left({X}\setminus {y}\right)\right)$
23 eldif ${⊢}{x}\in \left({X}\setminus {y}\right)↔\left({x}\in {X}\wedge ¬{x}\in {y}\right)$
24 23 baibr ${⊢}{x}\in {X}\to \left(¬{x}\in {y}↔{x}\in \left({X}\setminus {y}\right)\right)$
25 24 con1bid ${⊢}{x}\in {X}\to \left(¬{x}\in \left({X}\setminus {y}\right)↔{x}\in {y}\right)$
26 22 25 sylan9bb ${⊢}\left({c}={X}\setminus {y}\wedge {x}\in {X}\right)\to \left(¬{x}\in {c}↔{x}\in {y}\right)$
27 simpl ${⊢}\left({c}={X}\setminus {y}\wedge {x}\in {X}\right)\to {c}={X}\setminus {y}$
28 27 sseq1d ${⊢}\left({c}={X}\setminus {y}\wedge {x}\in {X}\right)\to \left({c}\subseteq {o}↔{X}\setminus {y}\subseteq {o}\right)$
29 28 3anbi1d ${⊢}\left({c}={X}\setminus {y}\wedge {x}\in {X}\right)\to \left(\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)↔\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)$
30 29 2rexbidv ${⊢}\left({c}={X}\setminus {y}\wedge {x}\in {X}\right)\to \left(\exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)↔\exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)$
31 26 30 imbi12d ${⊢}\left({c}={X}\setminus {y}\wedge {x}\in {X}\right)\to \left(\left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)↔\left({x}\in {y}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)$
32 31 ralbidva ${⊢}{c}={X}\setminus {y}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)$
33 32 rspcv ${⊢}{X}\setminus {y}\in \mathrm{Clsd}\left({J}\right)\to \left(\forall {c}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)$
34 20 33 syl ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\to \left(\forall {c}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)$
35 ralcom3 ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)↔\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {X}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)$
36 toponss ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\to {y}\subseteq {X}$
37 36 sselda ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\to {x}\in {X}$
38 simprr2 ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {x}\in {p}$
39 5 ad3antrrr ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {X}=\bigcup {J}$
40 39 difeq1d ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {X}\setminus {o}=\bigcup {J}\setminus {o}$
41 14 ad3antrrr ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {J}\in \mathrm{Top}$
42 simprll ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {o}\in {J}$
43 9 opncld ${⊢}\left({J}\in \mathrm{Top}\wedge {o}\in {J}\right)\to \bigcup {J}\setminus {o}\in \mathrm{Clsd}\left({J}\right)$
44 41 42 43 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to \bigcup {J}\setminus {o}\in \mathrm{Clsd}\left({J}\right)$
45 40 44 eqeltrd ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {X}\setminus {o}\in \mathrm{Clsd}\left({J}\right)$
46 incom ${⊢}{p}\cap {o}={o}\cap {p}$
47 simprr3 ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {o}\cap {p}=\varnothing$
48 46 47 syl5eq ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {p}\cap {o}=\varnothing$
49 simplll ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
50 simprlr ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {p}\in {J}$
51 toponss ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {p}\in {J}\right)\to {p}\subseteq {X}$
52 49 50 51 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {p}\subseteq {X}$
53 reldisj ${⊢}{p}\subseteq {X}\to \left({p}\cap {o}=\varnothing ↔{p}\subseteq {X}\setminus {o}\right)$
54 52 53 syl ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to \left({p}\cap {o}=\varnothing ↔{p}\subseteq {X}\setminus {o}\right)$
55 48 54 mpbid ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {p}\subseteq {X}\setminus {o}$
56 9 clsss2 ${⊢}\left({X}\setminus {o}\in \mathrm{Clsd}\left({J}\right)\wedge {p}\subseteq {X}\setminus {o}\right)\to \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {X}\setminus {o}$
57 45 55 56 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {X}\setminus {o}$
58 simprr1 ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {X}\setminus {y}\subseteq {o}$
59 difcom ${⊢}{X}\setminus {y}\subseteq {o}↔{X}\setminus {o}\subseteq {y}$
60 58 59 sylib ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {X}\setminus {o}\subseteq {y}$
61 57 60 sstrd ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}$
62 38 61 jca ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left(\left({o}\in {J}\wedge {p}\in {J}\right)\wedge \left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to \left({x}\in {p}\wedge \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}\right)$
63 62 expr ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge \left({o}\in {J}\wedge {p}\in {J}\right)\right)\to \left(\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\to \left({x}\in {p}\wedge \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}\right)\right)$
64 63 anassrs ${⊢}\left(\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge {o}\in {J}\right)\wedge {p}\in {J}\right)\to \left(\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\to \left({x}\in {p}\wedge \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}\right)\right)$
65 64 reximdva ${⊢}\left(\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\wedge {o}\in {J}\right)\to \left(\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\to \exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {p}\wedge \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}\right)\right)$
66 65 rexlimdva ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\to \left(\exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\to \exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {p}\wedge \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}\right)\right)$
67 37 66 embantd ${⊢}\left(\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\wedge {x}\in {y}\right)\to \left(\left({x}\in {X}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\to \exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {p}\wedge \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}\right)\right)$
68 67 ralimdva ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\to \left(\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {X}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\to \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {p}\wedge \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}\right)\right)$
69 35 68 syl5bi ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({X}\setminus {y}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\to \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {p}\wedge \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}\right)\right)$
70 34 69 syld ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {y}\in {J}\right)\to \left(\forall {c}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\to \forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {p}\wedge \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}\right)\right)$
71 70 ralrimdva ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left(\forall {c}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\to \forall {y}\in {J}\phantom{\rule{.4em}{0ex}}\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {p}\wedge \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}\right)\right)$
72 71 imp ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \forall {c}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to \forall {y}\in {J}\phantom{\rule{.4em}{0ex}}\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {p}\wedge \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}\right)$
73 isreg ${⊢}{J}\in \mathrm{Reg}↔\left({J}\in \mathrm{Top}\wedge \forall {y}\in {J}\phantom{\rule{.4em}{0ex}}\forall {x}\in {y}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({x}\in {p}\wedge \mathrm{cls}\left({J}\right)\left({p}\right)\subseteq {y}\right)\right)$
74 15 72 73 sylanbrc ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge \forall {c}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)\to {J}\in \mathrm{Reg}$
75 13 74 impbida ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \left({J}\in \mathrm{Reg}↔\forall {c}\in \mathrm{Clsd}\left({J}\right)\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(¬{x}\in {c}\to \exists {o}\in {J}\phantom{\rule{.4em}{0ex}}\exists {p}\in {J}\phantom{\rule{.4em}{0ex}}\left({c}\subseteq {o}\wedge {x}\in {p}\wedge {o}\cap {p}=\varnothing \right)\right)\right)$