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

Theorem regsep2 22089
 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 22046 . . . . . . 7 (𝐽 ∈ Reg → 𝐽 ∈ Top)
21ad2antrr 725 . . . . . 6 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝐽 ∈ Top)
3 elssuni 4833 . . . . . . . 8 (𝑦𝐽𝑦 𝐽)
4 t1sep.1 . . . . . . . 8 𝑋 = 𝐽
53, 4sseqtrrdi 3945 . . . . . . 7 (𝑦𝐽𝑦𝑋)
65ad2antrl 727 . . . . . 6 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝑦𝑋)
74clscld 21760 . . . . . 6 ((𝐽 ∈ Top ∧ 𝑦𝑋) → ((cls‘𝐽)‘𝑦) ∈ (Clsd‘𝐽))
82, 6, 7syl2anc 587 . . . . 5 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → ((cls‘𝐽)‘𝑦) ∈ (Clsd‘𝐽))
94cldopn 21744 . . . . 5 (((cls‘𝐽)‘𝑦) ∈ (Clsd‘𝐽) → (𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∈ 𝐽)
108, 9syl 17 . . . 4 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → (𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∈ 𝐽)
11 simprrr 781 . . . . 5 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶))
124clsss3 21772 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑦𝑋) → ((cls‘𝐽)‘𝑦) ⊆ 𝑋)
132, 6, 12syl2anc 587 . . . . . 6 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → ((cls‘𝐽)‘𝑦) ⊆ 𝑋)
14 simplr1 1212 . . . . . . 7 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝐶 ∈ (Clsd‘𝐽))
154cldss 21742 . . . . . . 7 (𝐶 ∈ (Clsd‘𝐽) → 𝐶𝑋)
1614, 15syl 17 . . . . . 6 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝐶𝑋)
17 ssconb 4045 . . . . . 6 ((((cls‘𝐽)‘𝑦) ⊆ 𝑋𝐶𝑋) → (((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶) ↔ 𝐶 ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝑦))))
1813, 16, 17syl2anc 587 . . . . 5 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → (((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶) ↔ 𝐶 ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝑦))))
1911, 18mpbid 235 . . . 4 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝐶 ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝑦)))
20 simprrl 780 . . . 4 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝐴𝑦)
214sscls 21769 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝑦𝑋) → 𝑦 ⊆ ((cls‘𝐽)‘𝑦))
222, 6, 21syl2anc 587 . . . . . 6 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → 𝑦 ⊆ ((cls‘𝐽)‘𝑦))
23 sslin 4141 . . . . . 6 (𝑦 ⊆ ((cls‘𝐽)‘𝑦) → ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) ⊆ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ ((cls‘𝐽)‘𝑦)))
2422, 23syl 17 . . . . 5 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) ⊆ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ ((cls‘𝐽)‘𝑦)))
25 incom 4108 . . . . . 6 ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ ((cls‘𝐽)‘𝑦)) = (((cls‘𝐽)‘𝑦) ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑦)))
26 disjdif 4371 . . . . . 6 (((cls‘𝐽)‘𝑦) ∩ (𝑋 ∖ ((cls‘𝐽)‘𝑦))) = ∅
2725, 26eqtri 2781 . . . . 5 ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ ((cls‘𝐽)‘𝑦)) = ∅
28 sseq0 4298 . . . . 5 ((((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) ⊆ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ ((cls‘𝐽)‘𝑦)) ∧ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ ((cls‘𝐽)‘𝑦)) = ∅) → ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) = ∅)
2924, 27, 28sylancl 589 . . . 4 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) = ∅)
30 sseq2 3920 . . . . . 6 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑦)) → (𝐶𝑥𝐶 ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝑦))))
31 ineq1 4111 . . . . . . 7 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑦)) → (𝑥𝑦) = ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦))
3231eqeq1d 2760 . . . . . 6 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑦)) → ((𝑥𝑦) = ∅ ↔ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) = ∅))
3330, 323anbi13d 1435 . . . . 5 (𝑥 = (𝑋 ∖ ((cls‘𝐽)‘𝑦)) → ((𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅) ↔ (𝐶 ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∧ 𝐴𝑦 ∧ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) = ∅)))
3433rspcev 3543 . . . 4 (((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∈ 𝐽 ∧ (𝐶 ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∧ 𝐴𝑦 ∧ ((𝑋 ∖ ((cls‘𝐽)‘𝑦)) ∩ 𝑦) = ∅)) → ∃𝑥𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅))
3510, 19, 20, 29, 34syl13anc 1369 . . 3 (((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) ∧ (𝑦𝐽 ∧ (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))) → ∃𝑥𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅))
36 simpl 486 . . . 4 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → 𝐽 ∈ Reg)
37 simpr1 1191 . . . . 5 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → 𝐶 ∈ (Clsd‘𝐽))
384cldopn 21744 . . . . 5 (𝐶 ∈ (Clsd‘𝐽) → (𝑋𝐶) ∈ 𝐽)
3937, 38syl 17 . . . 4 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → (𝑋𝐶) ∈ 𝐽)
40 simpr2 1192 . . . . 5 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → 𝐴𝑋)
41 simpr3 1193 . . . . 5 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → ¬ 𝐴𝐶)
4240, 41eldifd 3871 . . . 4 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → 𝐴 ∈ (𝑋𝐶))
43 regsep 22047 . . . 4 ((𝐽 ∈ Reg ∧ (𝑋𝐶) ∈ 𝐽𝐴 ∈ (𝑋𝐶)) → ∃𝑦𝐽 (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))
4436, 39, 42, 43syl3anc 1368 . . 3 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → ∃𝑦𝐽 (𝐴𝑦 ∧ ((cls‘𝐽)‘𝑦) ⊆ (𝑋𝐶)))
4535, 44reximddv 3199 . 2 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → ∃𝑦𝐽𝑥𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅))
46 rexcom 3273 . 2 (∃𝑦𝐽𝑥𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅) ↔ ∃𝑥𝐽𝑦𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅))
4745, 46sylib 221 1 ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴𝑋 ∧ ¬ 𝐴𝐶)) → ∃𝑥𝐽𝑦𝐽 (𝐶𝑥𝐴𝑦 ∧ (𝑥𝑦) = ∅))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∃wrex 3071   ∖ cdif 3857   ∩ cin 3859   ⊆ wss 3860  ∅c0 4227  ∪ cuni 4801  ‘cfv 6340  Topctop 21606  Clsdccld 21729  clsccl 21731  Regcreg 22022 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-iin 4889  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-top 21607  df-cld 21732  df-cls 21734  df-reg 22029 This theorem is referenced by:  isreg2  22090
 Copyright terms: Public domain W3C validator