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 ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Reg ↔ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑥 ∈ 𝑋 ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1r ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝑐 ) → 𝐽 ∈ Reg )
2 simp2l ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝑐 ) → 𝑐 ∈ ( Clsd ‘ 𝐽 ) )
3 simp2r ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝑐 ) → 𝑥 ∈ 𝑋 )
4 simp1l ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝑐 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
6 4 5 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝑐 ) → 𝑋 = ∪ 𝐽 )
7 3 6 eleqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝑐 ) → 𝑥 ∈ ∪ 𝐽 )
8 simp3 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝑐 ) → ¬ 𝑥 ∈ 𝑐 )
9 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
10 9 regsep2 ⊢ ( ( 𝐽 ∈ Reg ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ∈ ∪ 𝐽 ∧ ¬ 𝑥 ∈ 𝑐 ) ) → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) )
11 1 2 7 8 10 syl13anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ 𝑥 ∈ 𝑐 ) → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) )
12 11 3expia ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ∈ 𝑋 ) ) → ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) )
13 12 ralrimivva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ Reg ) → ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑥 ∈ 𝑋 ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) )
14 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
15 14 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑥 ∈ 𝑋 ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → 𝐽 ∈ Top )
16 5 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑋 = ∪ 𝐽 )
17 16 difeq1d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑋 ∖ 𝑦 ) = ( ∪ 𝐽 ∖ 𝑦 ) )
18 9 opncld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
19 14 18 sylan ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
20 17 19 eqeltrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑋 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
21 eleq2 ⊢ ( 𝑐 = ( 𝑋 ∖ 𝑦 ) → ( 𝑥 ∈ 𝑐 ↔ 𝑥 ∈ ( 𝑋 ∖ 𝑦 ) ) )
22 21 notbid ⊢ ( 𝑐 = ( 𝑋 ∖ 𝑦 ) → ( ¬ 𝑥 ∈ 𝑐 ↔ ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑦 ) ) )
23 eldif ⊢ ( 𝑥 ∈ ( 𝑋 ∖ 𝑦 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ 𝑦 ) )
24 23 baibr ⊢ ( 𝑥 ∈ 𝑋 → ( ¬ 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( 𝑋 ∖ 𝑦 ) ) )
25 24 con1bid ⊢ ( 𝑥 ∈ 𝑋 → ( ¬ 𝑥 ∈ ( 𝑋 ∖ 𝑦 ) ↔ 𝑥 ∈ 𝑦 ) )
26 22 25 sylan9bb ⊢ ( ( 𝑐 = ( 𝑋 ∖ 𝑦 ) ∧ 𝑥 ∈ 𝑋 ) → ( ¬ 𝑥 ∈ 𝑐 ↔ 𝑥 ∈ 𝑦 ) )
27 simpl ⊢ ( ( 𝑐 = ( 𝑋 ∖ 𝑦 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑐 = ( 𝑋 ∖ 𝑦 ) )
28 27 sseq1d ⊢ ( ( 𝑐 = ( 𝑋 ∖ 𝑦 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑐 ⊆ 𝑜 ↔ ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ) )
29 28 3anbi1d ⊢ ( ( 𝑐 = ( 𝑋 ∖ 𝑦 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ↔ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) )
30 29 2rexbidv ⊢ ( ( 𝑐 = ( 𝑋 ∖ 𝑦 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ↔ ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) )
31 26 30 imbi12d ⊢ ( ( 𝑐 = ( 𝑋 ∖ 𝑦 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ↔ ( 𝑥 ∈ 𝑦 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) )
32 31 ralbidva ⊢ ( 𝑐 = ( 𝑋 ∖ 𝑦 ) → ( ∀ 𝑥 ∈ 𝑋 ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ 𝑦 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) )
33 32 rspcv ⊢ ( ( 𝑋 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) → ( ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑥 ∈ 𝑋 ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ 𝑦 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) )
34 20 33 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → ( ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑥 ∈ 𝑋 ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ 𝑦 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) )
35 ralcom3 ⊢ ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ 𝑦 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ↔ ∀ 𝑥 ∈ 𝑦 ( 𝑥 ∈ 𝑋 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) )
36 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑦 ⊆ 𝑋 )
37 36 sselda ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ 𝑋 )
38 simprr2 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → 𝑥 ∈ 𝑝 )
39 5 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → 𝑋 = ∪ 𝐽 )
40 39 difeq1d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → ( 𝑋 ∖ 𝑜 ) = ( ∪ 𝐽 ∖ 𝑜 ) )
41 14 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → 𝐽 ∈ Top )
42 simprll ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → 𝑜 ∈ 𝐽 )
43 9 opncld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑜 ) ∈ ( Clsd ‘ 𝐽 ) )
44 41 42 43 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → ( ∪ 𝐽 ∖ 𝑜 ) ∈ ( Clsd ‘ 𝐽 ) )
45 40 44 eqeltrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → ( 𝑋 ∖ 𝑜 ) ∈ ( Clsd ‘ 𝐽 ) )
46 incom ⊢ ( 𝑝 ∩ 𝑜 ) = ( 𝑜 ∩ 𝑝 )
47 simprr3 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → ( 𝑜 ∩ 𝑝 ) = ∅ )
48 46 47 syl5eq ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → ( 𝑝 ∩ 𝑜 ) = ∅ )
49 simplll ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
50 simprlr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → 𝑝 ∈ 𝐽 )
51 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝐽 ) → 𝑝 ⊆ 𝑋 )
52 49 50 51 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → 𝑝 ⊆ 𝑋 )
53 reldisj ⊢ ( 𝑝 ⊆ 𝑋 → ( ( 𝑝 ∩ 𝑜 ) = ∅ ↔ 𝑝 ⊆ ( 𝑋 ∖ 𝑜 ) ) )
54 52 53 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → ( ( 𝑝 ∩ 𝑜 ) = ∅ ↔ 𝑝 ⊆ ( 𝑋 ∖ 𝑜 ) ) )
55 48 54 mpbid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → 𝑝 ⊆ ( 𝑋 ∖ 𝑜 ) )
56 9 clsss2 ⊢ ( ( ( 𝑋 ∖ 𝑜 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑝 ⊆ ( 𝑋 ∖ 𝑜 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ ( 𝑋 ∖ 𝑜 ) )
57 45 55 56 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ ( 𝑋 ∖ 𝑜 ) )
58 simprr1 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 )
59 difcom ⊢ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ↔ ( 𝑋 ∖ 𝑜 ) ⊆ 𝑦 )
60 58 59 sylib ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → ( 𝑋 ∖ 𝑜 ) ⊆ 𝑦 )
61 57 60 sstrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 )
62 38 61 jca ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ∧ ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → ( 𝑥 ∈ 𝑝 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 ) )
63 62 expr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) ) → ( ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) → ( 𝑥 ∈ 𝑝 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 ) ) )
64 63 anassrs ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑝 ∈ 𝐽 ) → ( ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) → ( 𝑥 ∈ 𝑝 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 ) ) )
65 64 reximdva ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑜 ∈ 𝐽 ) → ( ∃ 𝑝 ∈ 𝐽 ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) → ∃ 𝑝 ∈ 𝐽 ( 𝑥 ∈ 𝑝 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 ) ) )
66 65 rexlimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) → ( ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) → ∃ 𝑝 ∈ 𝐽 ( 𝑥 ∈ 𝑝 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 ) ) )
67 37 66 embantd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝑥 ∈ 𝑋 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) → ∃ 𝑝 ∈ 𝐽 ( 𝑥 ∈ 𝑝 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 ) ) )
68 67 ralimdva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 ∈ 𝑋 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) → ∀ 𝑥 ∈ 𝑦 ∃ 𝑝 ∈ 𝐽 ( 𝑥 ∈ 𝑝 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 ) ) )
69 35 68 syl5bi ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 ∈ 𝑦 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( ( 𝑋 ∖ 𝑦 ) ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) → ∀ 𝑥 ∈ 𝑦 ∃ 𝑝 ∈ 𝐽 ( 𝑥 ∈ 𝑝 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 ) ) )
70 34 69 syld ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → ( ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑥 ∈ 𝑋 ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) → ∀ 𝑥 ∈ 𝑦 ∃ 𝑝 ∈ 𝐽 ( 𝑥 ∈ 𝑝 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 ) ) )
71 70 ralrimdva ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑥 ∈ 𝑋 ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) → ∀ 𝑦 ∈ 𝐽 ∀ 𝑥 ∈ 𝑦 ∃ 𝑝 ∈ 𝐽 ( 𝑥 ∈ 𝑝 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 ) ) )
72 71 imp ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑥 ∈ 𝑋 ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → ∀ 𝑦 ∈ 𝐽 ∀ 𝑥 ∈ 𝑦 ∃ 𝑝 ∈ 𝐽 ( 𝑥 ∈ 𝑝 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 ) )
73 isreg ⊢ ( 𝐽 ∈ Reg ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝐽 ∀ 𝑥 ∈ 𝑦 ∃ 𝑝 ∈ 𝐽 ( 𝑥 ∈ 𝑝 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑝 ) ⊆ 𝑦 ) ) )
74 15 72 73 sylanbrc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑥 ∈ 𝑋 ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) → 𝐽 ∈ Reg )
75 13 74 impbida ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Reg ↔ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑥 ∈ 𝑋 ( ¬ 𝑥 ∈ 𝑐 → ∃ 𝑜 ∈ 𝐽 ∃ 𝑝 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ ( 𝑜 ∩ 𝑝 ) = ∅ ) ) ) )