Theorem haustop 23277

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.

Step	Hyp	Ref	Expression
1		eqid 2735	. . 3 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	ishaus 23268	. 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
3	2	simplbi 497	1 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2931  ∀wral 3050  ∃wrex 3059   ∩ cin 3899  ∅c0 4284  ∪ cuni 4862  Topctop 22839  Hauscha 23254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-ss 3917  df-uni 4863  df-haus 23261

This theorem is referenced by:  haust1  23298  resthaus  23314  sshaus  23321  lmmo  23326  hauscmplem  23352  hauscmp  23353  hauslly  23438  hausllycmp  23440  kgenhaus  23490  pthaus  23584  txhaus  23593  xkohaus  23599  haushmph  23738  cmphaushmeo  23746  hausflim  23927  hauspwpwf1  23933  hauspwpwdom  23934  hausflf  23943  cnextfun  24010  cnextfvval  24011  cnextf  24012  cnextcn  24013  cnextfres1  24014  cnextfres  24015  qtophaus  33972  ismntop  34162  poimirlem30  37820  hausgraph  43484