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

Theorem haust1 21888
Description: A Hausdorff space is a T1 space. (Contributed by FL, 11-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Aug-2015.)
Assertion
Ref Expression
haust1 (𝐽 ∈ Haus → 𝐽 ∈ Fre)

Proof of Theorem haust1
Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2818 . . . . . . . . 9 𝐽 = 𝐽
21hausnei 21864 . . . . . . . 8 ((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) → ∃𝑧𝐽𝑤𝐽 (𝑥𝑧𝑦𝑤 ∧ (𝑧𝑤) = ∅))
3 simprr1 1213 . . . . . . . . . . 11 ((((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) ∧ 𝑧𝐽) ∧ (𝑤𝐽 ∧ (𝑥𝑧𝑦𝑤 ∧ (𝑧𝑤) = ∅))) → 𝑥𝑧)
4 noel 4293 . . . . . . . . . . . . 13 ¬ 𝑦 ∈ ∅
5 simprr3 1215 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) ∧ 𝑧𝐽) ∧ (𝑤𝐽 ∧ (𝑥𝑧𝑦𝑤 ∧ (𝑧𝑤) = ∅))) → (𝑧𝑤) = ∅)
65eleq2d 2895 . . . . . . . . . . . . 13 ((((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) ∧ 𝑧𝐽) ∧ (𝑤𝐽 ∧ (𝑥𝑧𝑦𝑤 ∧ (𝑧𝑤) = ∅))) → (𝑦 ∈ (𝑧𝑤) ↔ 𝑦 ∈ ∅))
74, 6mtbiri 328 . . . . . . . . . . . 12 ((((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) ∧ 𝑧𝐽) ∧ (𝑤𝐽 ∧ (𝑥𝑧𝑦𝑤 ∧ (𝑧𝑤) = ∅))) → ¬ 𝑦 ∈ (𝑧𝑤))
8 simprr2 1214 . . . . . . . . . . . . 13 ((((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) ∧ 𝑧𝐽) ∧ (𝑤𝐽 ∧ (𝑥𝑧𝑦𝑤 ∧ (𝑧𝑤) = ∅))) → 𝑦𝑤)
9 elin 4166 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑧𝑤) ↔ (𝑦𝑧𝑦𝑤))
109simplbi2com 503 . . . . . . . . . . . . 13 (𝑦𝑤 → (𝑦𝑧𝑦 ∈ (𝑧𝑤)))
118, 10syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) ∧ 𝑧𝐽) ∧ (𝑤𝐽 ∧ (𝑥𝑧𝑦𝑤 ∧ (𝑧𝑤) = ∅))) → (𝑦𝑧𝑦 ∈ (𝑧𝑤)))
127, 11mtod 199 . . . . . . . . . . 11 ((((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) ∧ 𝑧𝐽) ∧ (𝑤𝐽 ∧ (𝑥𝑧𝑦𝑤 ∧ (𝑧𝑤) = ∅))) → ¬ 𝑦𝑧)
133, 12jca 512 . . . . . . . . . 10 ((((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) ∧ 𝑧𝐽) ∧ (𝑤𝐽 ∧ (𝑥𝑧𝑦𝑤 ∧ (𝑧𝑤) = ∅))) → (𝑥𝑧 ∧ ¬ 𝑦𝑧))
1413rexlimdvaa 3282 . . . . . . . . 9 (((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) ∧ 𝑧𝐽) → (∃𝑤𝐽 (𝑥𝑧𝑦𝑤 ∧ (𝑧𝑤) = ∅) → (𝑥𝑧 ∧ ¬ 𝑦𝑧)))
1514reximdva 3271 . . . . . . . 8 ((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) → (∃𝑧𝐽𝑤𝐽 (𝑥𝑧𝑦𝑤 ∧ (𝑧𝑤) = ∅) → ∃𝑧𝐽 (𝑥𝑧 ∧ ¬ 𝑦𝑧)))
162, 15mpd 15 . . . . . . 7 ((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) → ∃𝑧𝐽 (𝑥𝑧 ∧ ¬ 𝑦𝑧))
17 rexanali 3262 . . . . . . 7 (∃𝑧𝐽 (𝑥𝑧 ∧ ¬ 𝑦𝑧) ↔ ¬ ∀𝑧𝐽 (𝑥𝑧𝑦𝑧))
1816, 17sylib 219 . . . . . 6 ((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽𝑥𝑦)) → ¬ ∀𝑧𝐽 (𝑥𝑧𝑦𝑧))
19183exp2 1346 . . . . 5 (𝐽 ∈ Haus → (𝑥 𝐽 → (𝑦 𝐽 → (𝑥𝑦 → ¬ ∀𝑧𝐽 (𝑥𝑧𝑦𝑧)))))
2019imp32 419 . . . 4 ((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽)) → (𝑥𝑦 → ¬ ∀𝑧𝐽 (𝑥𝑧𝑦𝑧)))
2120necon4ad 3032 . . 3 ((𝐽 ∈ Haus ∧ (𝑥 𝐽𝑦 𝐽)) → (∀𝑧𝐽 (𝑥𝑧𝑦𝑧) → 𝑥 = 𝑦))
2221ralrimivva 3188 . 2 (𝐽 ∈ Haus → ∀𝑥 𝐽𝑦 𝐽(∀𝑧𝐽 (𝑥𝑧𝑦𝑧) → 𝑥 = 𝑦))
23 haustop 21867 . . . 4 (𝐽 ∈ Haus → 𝐽 ∈ Top)
24 toptopon2 21454 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
2523, 24sylib 219 . . 3 (𝐽 ∈ Haus → 𝐽 ∈ (TopOn‘ 𝐽))
26 ist1-2 21883 . . 3 (𝐽 ∈ (TopOn‘ 𝐽) → (𝐽 ∈ Fre ↔ ∀𝑥 𝐽𝑦 𝐽(∀𝑧𝐽 (𝑥𝑧𝑦𝑧) → 𝑥 = 𝑦)))
2725, 26syl 17 . 2 (𝐽 ∈ Haus → (𝐽 ∈ Fre ↔ ∀𝑥 𝐽𝑦 𝐽(∀𝑧𝐽 (𝑥𝑧𝑦𝑧) → 𝑥 = 𝑦)))
2822, 27mpbird 258 1 (𝐽 ∈ Haus → 𝐽 ∈ Fre)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  cin 3932  c0 4288   cuni 4830  cfv 6348  Topctop 21429  TopOnctopon 21446  Frect1 21843  Hauscha 21844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356  df-topgen 16705  df-top 21430  df-topon 21447  df-cld 21555  df-t1 21850  df-haus 21851
This theorem is referenced by:  sncld  21907  ishaus3  22359  reghaus  22361  nrmhaus  22362  tgpt1  22653  metreg  23398  ipasslem8  28541  sitmcl  31508  onint1  33694  oninhaus  33695  poimirlem30  34803
  Copyright terms: Public domain W3C validator