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

Theorem haustop 21356
 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 2771 . . 3 𝐽 = 𝐽
21ishaus 21347 . 2 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑛𝐽𝑚𝐽 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))))
32simplbi 485 1 (𝐽 ∈ Haus → 𝐽 ∈ Top)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1071   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  ∀wral 3061  ∃wrex 3062   ∩ cin 3722  ∅c0 4063  ∪ cuni 4575  Topctop 20918  Hauscha 21333 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-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-uni 4576  df-haus 21340 This theorem is referenced by:  haust1  21377  resthaus  21393  sshaus  21400  lmmo  21405  hauscmplem  21430  hauscmp  21431  hauslly  21516  hausllycmp  21518  kgenhaus  21568  pthaus  21662  txhaus  21671  xkohaus  21677  haushmph  21816  cmphaushmeo  21824  hausflim  22005  hauspwpwf1  22011  hauspwpwdom  22012  hausflf  22021  cnextfun  22088  cnextfvval  22089  cnextf  22090  cnextcn  22091  cnextfres1  22092  cnextfres  22093  qtophaus  30243  ismntop  30410  poimirlem30  33772  hausgraph  38316
 Copyright terms: Public domain W3C validator