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

Theorem haustop 21506
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 2825 . . 3 𝐽 = 𝐽
21ishaus 21497 . 2 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑛𝐽𝑚𝐽 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))))
32simplbi 493 1 (𝐽 ∈ Haus → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1113   = wceq 1658  wcel 2166  wne 2999  wral 3117  wrex 3118  cin 3797  c0 4144   cuni 4658  Topctop 21068  Hauscha 21483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-uni 4659  df-haus 21490
This theorem is referenced by:  haust1  21527  resthaus  21543  sshaus  21550  lmmo  21555  hauscmplem  21580  hauscmp  21581  hauslly  21666  hausllycmp  21668  kgenhaus  21718  pthaus  21812  txhaus  21821  xkohaus  21827  haushmph  21966  cmphaushmeo  21974  hausflim  22155  hauspwpwf1  22161  hauspwpwdom  22162  hausflf  22171  cnextfun  22238  cnextfvval  22239  cnextf  22240  cnextcn  22241  cnextfres1  22242  cnextfres  22243  qtophaus  30448  ismntop  30615  poimirlem30  33983  hausgraph  38633
  Copyright terms: Public domain W3C validator