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

Theorem isreg2 21920
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 1192 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → 𝐽 ∈ Reg)
2 simp2l 1193 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → 𝑐 ∈ (Clsd‘𝐽))
3 simp2r 1194 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → 𝑥𝑋)
4 simp1l 1191 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → 𝐽 ∈ (TopOn‘𝑋))
5 toponuni 21457 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
64, 5syl 17 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → 𝑋 = 𝐽)
73, 6eleqtrd 2920 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → 𝑥 𝐽)
8 simp3 1132 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → ¬ 𝑥𝑐)
9 eqid 2826 . . . . . 6 𝐽 = 𝐽
109regsep2 21919 . . . . 5 ((𝐽 ∈ Reg ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥 𝐽 ∧ ¬ 𝑥𝑐)) → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))
111, 2, 7, 8, 10syl13anc 1366 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋) ∧ ¬ 𝑥𝑐) → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))
12113expia 1115 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) ∧ (𝑐 ∈ (Clsd‘𝐽) ∧ 𝑥𝑋)) → (¬ 𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)))
1312ralrimivva 3196 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → ∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)))
14 topontop 21456 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
1514adantr 481 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝐽 ∈ Top)
165adantr 481 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → 𝑋 = 𝐽)
1716difeq1d 4102 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → (𝑋𝑦) = ( 𝐽𝑦))
189opncld 21576 . . . . . . . . 9 ((𝐽 ∈ Top ∧ 𝑦𝐽) → ( 𝐽𝑦) ∈ (Clsd‘𝐽))
1914, 18sylan 580 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → ( 𝐽𝑦) ∈ (Clsd‘𝐽))
2017, 19eqeltrd 2918 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → (𝑋𝑦) ∈ (Clsd‘𝐽))
21 eleq2 2906 . . . . . . . . . . . 12 (𝑐 = (𝑋𝑦) → (𝑥𝑐𝑥 ∈ (𝑋𝑦)))
2221notbid 319 . . . . . . . . . . 11 (𝑐 = (𝑋𝑦) → (¬ 𝑥𝑐 ↔ ¬ 𝑥 ∈ (𝑋𝑦)))
23 eldif 3950 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑋𝑦) ↔ (𝑥𝑋 ∧ ¬ 𝑥𝑦))
2423baibr 537 . . . . . . . . . . . 12 (𝑥𝑋 → (¬ 𝑥𝑦𝑥 ∈ (𝑋𝑦)))
2524con1bid 357 . . . . . . . . . . 11 (𝑥𝑋 → (¬ 𝑥 ∈ (𝑋𝑦) ↔ 𝑥𝑦))
2622, 25sylan9bb 510 . . . . . . . . . 10 ((𝑐 = (𝑋𝑦) ∧ 𝑥𝑋) → (¬ 𝑥𝑐𝑥𝑦))
27 simpl 483 . . . . . . . . . . . . 13 ((𝑐 = (𝑋𝑦) ∧ 𝑥𝑋) → 𝑐 = (𝑋𝑦))
2827sseq1d 4002 . . . . . . . . . . . 12 ((𝑐 = (𝑋𝑦) ∧ 𝑥𝑋) → (𝑐𝑜 ↔ (𝑋𝑦) ⊆ 𝑜))
29283anbi1d 1433 . . . . . . . . . . 11 ((𝑐 = (𝑋𝑦) ∧ 𝑥𝑋) → ((𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅) ↔ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)))
30292rexbidv 3305 . . . . . . . . . 10 ((𝑐 = (𝑋𝑦) ∧ 𝑥𝑋) → (∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅) ↔ ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)))
3126, 30imbi12d 346 . . . . . . . . 9 ((𝑐 = (𝑋𝑦) ∧ 𝑥𝑋) → ((¬ 𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) ↔ (𝑥𝑦 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))))
3231ralbidva 3201 . . . . . . . 8 (𝑐 = (𝑋𝑦) → (∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) ↔ ∀𝑥𝑋 (𝑥𝑦 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))))
3332rspcv 3622 . . . . . . 7 ((𝑋𝑦) ∈ (Clsd‘𝐽) → (∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∀𝑥𝑋 (𝑥𝑦 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))))
3420, 33syl 17 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → (∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∀𝑥𝑋 (𝑥𝑦 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))))
35 ralcom3 3370 . . . . . . 7 (∀𝑥𝑋 (𝑥𝑦 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) ↔ ∀𝑥𝑦 (𝑥𝑋 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)))
36 toponss 21470 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → 𝑦𝑋)
3736sselda 3971 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) → 𝑥𝑋)
38 simprr2 1216 . . . . . . . . . . . . . 14 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝑥𝑝)
395ad3antrrr 726 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝑋 = 𝐽)
4039difeq1d 4102 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑋𝑜) = ( 𝐽𝑜))
4114ad3antrrr 726 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝐽 ∈ Top)
42 simprll 775 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝑜𝐽)
439opncld 21576 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑜𝐽) → ( 𝐽𝑜) ∈ (Clsd‘𝐽))
4441, 42, 43syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → ( 𝐽𝑜) ∈ (Clsd‘𝐽))
4540, 44eqeltrd 2918 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑋𝑜) ∈ (Clsd‘𝐽))
46 incom 4182 . . . . . . . . . . . . . . . . . 18 (𝑝𝑜) = (𝑜𝑝)
47 simprr3 1217 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑜𝑝) = ∅)
4846, 47syl5eq 2873 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑝𝑜) = ∅)
49 simplll 771 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝐽 ∈ (TopOn‘𝑋))
50 simprlr 776 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝑝𝐽)
51 toponss 21470 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑝𝐽) → 𝑝𝑋)
5249, 50, 51syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝑝𝑋)
53 reldisj 4405 . . . . . . . . . . . . . . . . . 18 (𝑝𝑋 → ((𝑝𝑜) = ∅ ↔ 𝑝 ⊆ (𝑋𝑜)))
5452, 53syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → ((𝑝𝑜) = ∅ ↔ 𝑝 ⊆ (𝑋𝑜)))
5548, 54mpbid 233 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝑝 ⊆ (𝑋𝑜))
569clsss2 21615 . . . . . . . . . . . . . . . 16 (((𝑋𝑜) ∈ (Clsd‘𝐽) ∧ 𝑝 ⊆ (𝑋𝑜)) → ((cls‘𝐽)‘𝑝) ⊆ (𝑋𝑜))
5745, 55, 56syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → ((cls‘𝐽)‘𝑝) ⊆ (𝑋𝑜))
58 simprr1 1215 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑋𝑦) ⊆ 𝑜)
59 difcom 4437 . . . . . . . . . . . . . . . 16 ((𝑋𝑦) ⊆ 𝑜 ↔ (𝑋𝑜) ⊆ 𝑦)
6058, 59sylib 219 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑋𝑜) ⊆ 𝑦)
6157, 60sstrd 3981 . . . . . . . . . . . . . 14 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → ((cls‘𝐽)‘𝑝) ⊆ 𝑦)
6238, 61jca 512 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ ((𝑜𝐽𝑝𝐽) ∧ ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦))
6362expr 457 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ (𝑜𝐽𝑝𝐽)) → (((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅) → (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
6463anassrs 468 . . . . . . . . . . 11 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ 𝑜𝐽) ∧ 𝑝𝐽) → (((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅) → (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
6564reximdva 3279 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) ∧ 𝑜𝐽) → (∃𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅) → ∃𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
6665rexlimdva 3289 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) → (∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅) → ∃𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
6737, 66embantd 59 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) ∧ 𝑥𝑦) → ((𝑥𝑋 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∃𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
6867ralimdva 3182 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → (∀𝑥𝑦 (𝑥𝑋 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∀𝑥𝑦𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
6935, 68syl5bi 243 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → (∀𝑥𝑋 (𝑥𝑦 → ∃𝑜𝐽𝑝𝐽 ((𝑋𝑦) ⊆ 𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∀𝑥𝑦𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
7034, 69syld 47 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦𝐽) → (∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∀𝑥𝑦𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
7170ralrimdva 3194 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅)) → ∀𝑦𝐽𝑥𝑦𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
7271imp 407 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → ∀𝑦𝐽𝑥𝑦𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦))
73 isreg 21875 . . 3 (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑦𝐽𝑥𝑦𝑝𝐽 (𝑥𝑝 ∧ ((cls‘𝐽)‘𝑝) ⊆ 𝑦)))
7415, 72, 73sylanbrc 583 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))) → 𝐽 ∈ Reg)
7513, 74impbida 797 1 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Reg ↔ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑥𝑋𝑥𝑐 → ∃𝑜𝐽𝑝𝐽 (𝑐𝑜𝑥𝑝 ∧ (𝑜𝑝) = ∅))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  wral 3143  wrex 3144  cdif 3937  cin 3939  wss 3940  c0 4295   cuni 4837  cfv 6354  Topctop 21436  TopOnctopon 21453  Clsdccld 21559  clsccl 21561  Regcreg 21852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-top 21437  df-topon 21454  df-cld 21562  df-cls 21564  df-reg 21859
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator