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

Theorem regsep2 21401
Description: In a regular space, a closed set is separated by open sets from a point not in it. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.)
Hypothesis
Ref Expression
t1sep.1 𝑋 = 𝐽
Assertion
Ref Expression
regsep2 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → ∃𝑥𝐽𝑦𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐶,𝑦   𝑥,𝐽,𝑦   𝑥,𝑋,𝑦

Proof of Theorem regsep2
StepHypRef Expression
1 regtop 21358 . . . . . . 7 (𝐽 ∈ Reg → 𝐽 ∈ Top)
21ad2antrr 705 . . . . . 6 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝐽 ∈ Top)
3 elssuni 4603 . . . . . . . 8 (𝑦𝐽𝑦 𝐽)
4 t1sep.1 . . . . . . . 8 𝑋 = 𝐽
53, 4syl6sseqr 3801 . . . . . . 7 (𝑦𝐽𝑦𝑋)
65ad2antrl 707 . . . . . 6 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝑦𝑋)
74clscld 21072 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑦𝑋) → ((cls‘𝐽)‘𝑦) ∈ (Clsd‘𝐽))
82, 6, 7syl2anc 573 . . . . 5 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → ((cls‘𝐽)‘𝑦) ∈ (Clsd‘𝐽))
94cldopn 21056 . . . . 5 (((cls‘𝐽)‘𝑦) ∈ (Clsd‘𝐽) → (𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∈ 𝐽)
108, 9syl 17 . . . 4 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → (𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∈ 𝐽)
11 simprrr 767 . . . . 5 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶))
124clsss3 21084 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑦𝑋) → ((cls‘𝐽)‘𝑦) ⊆ 𝑋)
132, 6, 12syl2anc 573 . . . . . 6 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → ((cls‘𝐽)‘𝑦) ⊆ 𝑋)
14 simplr1 1260 . . . . . . 7 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝐶 ∈ (Clsd‘𝐽))
154cldss 21054 . . . . . . 7 (𝐶 ∈ (Clsd‘𝐽) → 𝐶𝑋)
1614, 15syl 17 . . . . . 6 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝐶𝑋)
17 ssconb 3894 . . . . . 6 ((((cls‘𝐽)‘𝑦) ⊆ 𝑋𝐶𝑋) → (((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶) ↔ 𝐶 ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝑦))))
1813, 16, 17syl2anc 573 . . . . 5 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → (((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶) ↔ 𝐶 ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝑦))))
1911, 18mpbid 222 . . . 4 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝐶 ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝑦)))
20 simprrl 766 . . . 4 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝐴𝑦)
214sscls 21081 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑦𝑋) → 𝑦 ⊆ ((cls‘𝐽)‘𝑦))
222, 6, 21syl2anc 573 . . . . . 6 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝑦 ⊆ ((cls‘𝐽)‘𝑦))
23 sslin 3987 . . . . . 6 (𝑦 ⊆ ((cls‘𝐽)‘𝑦) → ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) ⊆ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ ((cls‘𝐽)‘𝑦)))
2422, 23syl 17 . . . . 5 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) ⊆ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ ((cls‘𝐽)‘𝑦)))
25 incom 3956 . . . . . 6 ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ ((cls‘𝐽)‘𝑦)) = (((cls‘𝐽)‘𝑦) ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑦)))
26 disjdif 4182 . . . . . 6 (((cls‘𝐽)‘𝑦) ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑦))) = ∅
2725, 26eqtri 2793 . . . . 5 ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ ((cls‘𝐽)‘𝑦)) = ∅
28 sseq0 4119 . . . . 5 ((((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) ⊆ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ ((cls‘𝐽)‘𝑦)) ∧ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ ((cls‘𝐽)‘𝑦)) = ∅) → ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) = ∅)
2924, 27, 28sylancl 574 . . . 4 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) = ∅)
30 sseq2 3776 . . . . . 6 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑦)) → (𝐶𝑥𝐶 ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝑦))))
31 ineq1 3958 . . . . . . 7 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑦)) → (𝑥𝑦) = ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦))
3231eqeq1d 2773 . . . . . 6 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑦)) → ((𝑥𝑦) = ∅ ↔ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) = ∅))
3330, 323anbi13d 1549 . . . . 5 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑦)) → ((𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅) ↔ (𝐶 ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∧ 𝐴𝑦 ∧ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) = ∅)))
3433rspcev 3460 . . . 4 (((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∈ 𝐽 ∧ (𝐶 ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∧ 𝐴𝑦 ∧ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) = ∅)) → ∃𝑥𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅))
3510, 19, 20, 29, 34syl13anc 1478 . . 3 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → ∃𝑥𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅))
36 simpl 468 . . . 4 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → 𝐽 ∈ Reg)
37 simpr1 1233 . . . . 5 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → 𝐶 ∈ (Clsd‘𝐽))
384cldopn 21056 . . . . 5 (𝐶 ∈ (Clsd‘𝐽) → (𝑋𝐶) ∈ 𝐽)
3937, 38syl 17 . . . 4 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → (𝑋𝐶) ∈ 𝐽)
40 simpr2 1235 . . . . 5 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → 𝐴𝑋)
41 simpr3 1237 . . . . 5 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → ¬ 𝐴𝐶)
4240, 41eldifd 3734 . . . 4 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → 𝐴 ∈ (𝑋𝐶))
43 regsep 21359 . . . 4 ((𝐽 ∈ Reg ∧ (𝑋𝐶) ∈ 𝐽𝐴 ∈ (𝑋𝐶)) → ∃𝑦𝐽 (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))
4436, 39, 42, 43syl3anc 1476 . . 3 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → ∃𝑦𝐽 (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))
4535, 44reximddv 3166 . 2 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → ∃𝑦𝐽𝑥𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅))
46 rexcom 3247 . 2 (∃𝑦𝐽𝑥𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅) ↔ ∃𝑥𝐽𝑦𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅))
4745, 46sylib 208 1 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → ∃𝑥𝐽𝑦𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wrex 3062  cdif 3720  cin 3722  wss 3723  c0 4063   cuni 4574  cfv 6031  Topctop 20918  Clsdccld 21041  clsccl 21043  Regcreg 21334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-top 20919  df-cld 21044  df-cls 21046  df-reg 21341
This theorem is referenced by:  isreg2  21402
  Copyright terms: Public domain W3C validator