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

Theorem haustop 22835
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 2733 . . 3 𝐽 = 𝐽
21ishaus 22826 . 2 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑛𝐽𝑚𝐽 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))))
32simplbi 499 1 (𝐽 ∈ Haus → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088   = wceq 1542  wcel 2107  wne 2941  wral 3062  wrex 3071  cin 3948  c0 4323   cuni 4909  Topctop 22395  Hauscha 22812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-haus 22819
This theorem is referenced by:  haust1  22856  resthaus  22872  sshaus  22879  lmmo  22884  hauscmplem  22910  hauscmp  22911  hauslly  22996  hausllycmp  22998  kgenhaus  23048  pthaus  23142  txhaus  23151  xkohaus  23157  haushmph  23296  cmphaushmeo  23304  hausflim  23485  hauspwpwf1  23491  hauspwpwdom  23492  hausflf  23501  cnextfun  23568  cnextfvval  23569  cnextf  23570  cnextcn  23571  cnextfres1  23572  cnextfres  23573  qtophaus  32816  ismntop  33006  poimirlem30  36518  hausgraph  41954
  Copyright terms: Public domain W3C validator