MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isreg2 Structured version   Visualization version   GIF version

Theorem isreg2 21510
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.)
Assertion
Ref Expression
isreg2 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Reg ↔ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))))
Distinct variable groups:   𝑜,𝑐,𝑝,𝑥,𝐽   𝑋,𝑐,𝑜,𝑝,𝑥

Proof of Theorem isreg2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 simp1r 1256 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → 𝐽 ∈ Reg)
2 simp2l 1257 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → 𝑐 ∈ (Clsd‘𝐽))
3 simp2r 1258 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → 𝑥𝑋)
4 simp1l 1255 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → 𝐽 ∈ (TopOn‘𝑋))
5 toponuni 21047 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
64, 5syl 17 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → 𝑋 = 𝐽)
73, 6eleqtrd 2880 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → 𝑥 𝐽)
8 simp3 1169 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → ¬ 𝑥𝑐)
9 eqid 2799 . . . . . 6 𝐽 = 𝐽
109regsep2 21509 . . . . 5 ((𝐽 ∈ Reg ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥 𝐽 ∧ ¬ 𝑥𝑐)) → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))
111, 2, 7, 8, 10syl13anc 1492 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))
12113expia 1151 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋)) → (¬ 𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)))
1312ralrimivva 3152 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → ∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)))
14 topontop 21046 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
1514adantr 473 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝐽 ∈ Top)
165adantr 473 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → 𝑋 = 𝐽)
1716difeq1d 3925 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → (𝑋𝑦) = ( 𝐽𝑦))
189opncld 21166 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑦𝐽) → ( 𝐽𝑦) ∈ (Clsd‘𝐽))
1914, 18sylan 576 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → ( 𝐽𝑦) ∈ (Clsd‘𝐽))
2017, 19eqeltrd 2878 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
21 eleq2 2867 . . . . . . . . . . . 12 (𝑐 = (𝑋𝑦) → (𝑥𝑐𝑥 ∈ (𝑋𝑦)))
2221notbid 310 . . . . . . . . . . 11 (𝑐 = (𝑋𝑦) → (¬ 𝑥𝑐 ↔ ¬ 𝑥 ∈ (𝑋𝑦)))
23 eldif 3779 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑋𝑦) ↔ (𝑥𝑋 ∧ ¬ 𝑥𝑦))
2423baibr 533 . . . . . . . . . . . 12 (𝑥𝑋 → (¬ 𝑥𝑦𝑥 ∈ (𝑋𝑦)))
2524con1bid 347 . . . . . . . . . . 11 (𝑥𝑋 → (¬ 𝑥 ∈ (𝑋𝑦) ↔ 𝑥𝑦))
2622, 25sylan9bb 506 . . . . . . . . . 10 ((𝑐 = (𝑋𝑦) ∧ 𝑥𝑋) → (¬ 𝑥𝑐𝑥𝑦))
27 simpl 475 . . . . . . . . . . . . 13 ((𝑐 = (𝑋𝑦) ∧ 𝑥𝑋) → 𝑐 = (𝑋𝑦))
2827sseq1d 3828 . . . . . . . . . . . 12 ((𝑐 = (𝑋𝑦) ∧ 𝑥𝑋) → (𝑐𝑜 ↔ (𝑋𝑦) ⊆ 𝑜))
29283anbi1d 1565 . . . . . . . . . . 11 ((𝑐 = (𝑋𝑦) ∧ 𝑥𝑋) → ((𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅) ↔ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)))
30292rexbidv 3238 . . . . . . . . . 10 ((𝑐 = (𝑋𝑦) ∧ 𝑥𝑋) → (∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅) ↔ ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)))
3126, 30imbi12d 336 . . . . . . . . 9 ((𝑐 = (𝑋𝑦) ∧ 𝑥𝑋) → ((¬ 𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) ↔ (𝑥𝑦 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))))
3231ralbidva 3166 . . . . . . . 8 (𝑐 = (𝑋𝑦) → (∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) ↔ ∀𝑥𝑋 (𝑥𝑦 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))))
3332rspcv 3493 . . . . . . 7 ((𝑋𝑦) ∈ (Clsd‘𝐽) → (∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∀𝑥𝑋 (𝑥𝑦 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))))
3420, 33syl 17 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → (∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∀𝑥𝑋 (𝑥𝑦 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))))
35 ralcom3 3286 . . . . . . 7 (∀𝑥𝑋 (𝑥𝑦 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) ↔ ∀𝑥𝑦 (𝑥𝑋 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)))
36 toponss 21060 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → 𝑦𝑋)
3736sselda 3798 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) → 𝑥𝑋)
38 simprr2 1290 . . . . . . . . . . . . . 14 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝑥𝑝)
395ad3antrrr 722 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝑋 = 𝐽)
4039difeq1d 3925 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑋𝑜) = ( 𝐽𝑜))
4114ad3antrrr 722 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝐽 ∈ Top)
42 simprll 798 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝑜𝐽)
439opncld 21166 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑜𝐽) → ( 𝐽𝑜) ∈ (Clsd‘𝐽))
4441, 42, 43syl2anc 580 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → ( 𝐽𝑜) ∈ (Clsd‘𝐽))
4540, 44eqeltrd 2878 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑋𝑜) ∈ (Clsd‘𝐽))
46 incom 4003 . . . . . . . . . . . . . . . . . 18 (𝑝𝑜) = (𝑜𝑝)
47 simprr3 1292 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑜𝑝) = ∅)
4846, 47syl5eq 2845 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑝𝑜) = ∅)
49 simplll 792 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝐽 ∈ (TopOn‘𝑋))
50 simprlr 799 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝑝𝐽)
51 toponss 21060 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑝𝐽) → 𝑝𝑋)
5249, 50, 51syl2anc 580 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝑝𝑋)
53 reldisj 4215 . . . . . . . . . . . . . . . . . 18 (𝑝𝑋 → ((𝑝𝑜) = ∅ ↔ 𝑝 ⊆ (𝑋𝑜)))
5452, 53syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → ((𝑝𝑜) = ∅ ↔ 𝑝 ⊆ (𝑋𝑜)))
5548, 54mpbid 224 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝑝 ⊆ (𝑋𝑜))
569clsss2 21205 . . . . . . . . . . . . . . . 16 (((𝑋𝑜) ∈ (Clsd‘𝐽) ∧ 𝑝 ⊆ (𝑋𝑜)) → ((cls‘𝐽)‘𝑝) ⊆ (𝑋𝑜))
5745, 55, 56syl2anc 580 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → ((cls‘𝐽)‘𝑝) ⊆ (𝑋𝑜))
58 simprr1 1288 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑋𝑦) ⊆ 𝑜)
59 difcom 4247 . . . . . . . . . . . . . . . 16 ((𝑋𝑦) ⊆ 𝑜 ↔ (𝑋𝑜) ⊆ 𝑦)
6058, 59sylib 210 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑋𝑜) ⊆ 𝑦)
6157, 60sstrd 3808 . . . . . . . . . . . . . 14 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → ((cls‘𝐽)‘𝑝) ⊆ 𝑦)
6238, 61jca 508 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦))
6362expr 449 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ (𝑜𝐽𝑝𝐽)) → (((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅) → (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
6463anassrs 460 . . . . . . . . . . 11 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ 𝑜𝐽) ∧ 𝑝𝐽) → (((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅) → (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
6564reximdva 3197 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ 𝑜𝐽) → (∃𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅) → ∃𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
6665rexlimdva 3212 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) → (∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅) → ∃𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
6737, 66embantd 59 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) → ((𝑥𝑋 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∃𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
6867ralimdva 3143 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → (∀𝑥𝑦 (𝑥𝑋 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∀𝑥𝑦𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
6935, 68syl5bi 234 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → (∀𝑥𝑋 (𝑥𝑦 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∀𝑥𝑦𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
7034, 69syld 47 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → (∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∀𝑥𝑦𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
7170ralrimdva 3150 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∀𝑦𝐽𝑥𝑦𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
7271imp 396 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → ∀𝑦𝐽𝑥𝑦𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦))
73 isreg 21465 . . 3 (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑦𝐽𝑥𝑦𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
7415, 72, 73sylanbrc 579 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝐽 ∈ Reg)
7513, 74impbida 836 1 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Reg ↔ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 385  w3a 1108   = wceq 1653  wcel 2157  wral 3089  wrex 3090  cdif 3766  cin 3768  wss 3769  c0 4115   cuni 4628  cfv 6101  Topctop 21026  TopOnctopon 21043  Clsdccld 21149  clsccl 21151  Regcreg 21442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5097  ax-un 7183
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3387  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-int 4668  df-iun 4712  df-iin 4713  df-br 4844  df-opab 4906  df-mpt 4923  df-id 5220  df-xp 5318  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-rn 5323  df-res 5324  df-ima 5325  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-top 21027  df-topon 21044  df-cld 21152  df-cls 21154  df-reg 21449
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator