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

Theorem haustop 21855
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 2826 . . 3 𝐽 = 𝐽
21ishaus 21846 . 2 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑛𝐽𝑚𝐽 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))))
32simplbi 498 1 (𝐽 ∈ Haus → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081   = wceq 1530  wcel 2107  wne 3021  wral 3143  wrex 3144  cin 3939  c0 4295   cuni 4837  Topctop 21417  Hauscha 21832
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-uni 4838  df-haus 21839
This theorem is referenced by:  haust1  21876  resthaus  21892  sshaus  21899  lmmo  21904  hauscmplem  21930  hauscmp  21931  hauslly  22016  hausllycmp  22018  kgenhaus  22068  pthaus  22162  txhaus  22171  xkohaus  22177  haushmph  22316  cmphaushmeo  22324  hausflim  22505  hauspwpwf1  22511  hauspwpwdom  22512  hausflf  22521  cnextfun  22588  cnextfvval  22589  cnextf  22590  cnextcn  22591  cnextfres1  22592  cnextfres  22593  qtophaus  30986  ismntop  31153  poimirlem30  34789  hausgraph  39677
  Copyright terms: Public domain W3C validator