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.

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

Syntax hints:   → wi 4   ∧ w3a 1071   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  ∀wral 3061  ∃wrex 3062   ∩ cin 3722  ∅c0 4063  ∪ cuni 4574  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 4575  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