Theorem haustop 23274

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 2736	. . 3 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	ishaus 23265	. 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
3	2	simplbi 497	1 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2933  ∀wral 3052  ∃wrex 3061   ∩ cin 3930  ∅c0 4313  ∪ cuni 4888  Topctop 22836  Hauscha 23251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-ss 3948  df-uni 4889  df-haus 23258

This theorem is referenced by:  haust1  23295  resthaus  23311  sshaus  23318  lmmo  23323  hauscmplem  23349  hauscmp  23350  hauslly  23435  hausllycmp  23437  kgenhaus  23487  pthaus  23581  txhaus  23590  xkohaus  23596  haushmph  23735  cmphaushmeo  23743  hausflim  23924  hauspwpwf1  23930  hauspwpwdom  23931  hausflf  23940  cnextfun  24007  cnextfvval  24008  cnextf  24009  cnextcn  24010  cnextfres1  24011  cnextfres  24012  qtophaus  33872  ismntop  34062  poimirlem30  37679  hausgraph  43204