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.

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

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