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

Theorem haustop 23279
Description: A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.)
Assertion
Ref Expression
haustop (𝐽 ∈ Haus → 𝐽 ∈ Top)

Proof of Theorem haustop
Dummy variables 𝑥 𝑦 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2725 . . 3 𝐽 = 𝐽
21ishaus 23270 . 2 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑛𝐽𝑚𝐽 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))))
32simplbi 496 1 (𝐽 ∈ Haus → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084   = wceq 1533  wcel 2098  wne 2929  wral 3050  wrex 3059  cin 3943  c0 4322   cuni 4909  Topctop 22839  Hauscha 23256
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-ss 3961  df-uni 4910  df-haus 23263
This theorem is referenced by:  haust1  23300  resthaus  23316  sshaus  23323  lmmo  23328  hauscmplem  23354  hauscmp  23355  hauslly  23440  hausllycmp  23442  kgenhaus  23492  pthaus  23586  txhaus  23595  xkohaus  23601  haushmph  23740  cmphaushmeo  23748  hausflim  23929  hauspwpwf1  23935  hauspwpwdom  23936  hausflf  23945  cnextfun  24012  cnextfvval  24013  cnextf  24014  cnextcn  24015  cnextfres1  24016  cnextfres  24017  qtophaus  33568  ismntop  33758  poimirlem30  37254  hausgraph  42775
  Copyright terms: Public domain W3C validator