Theorem haustop 22834

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2940  ∀wral 3061  ∃wrex 3070   ∩ cin 3947  ∅c0 4322  ∪ cuni 4908  Topctop 22394  Hauscha 22811

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909  df-haus 22818

This theorem is referenced by:  haust1  22855  resthaus  22871  sshaus  22878  lmmo  22883  hauscmplem  22909  hauscmp  22910  hauslly  22995  hausllycmp  22997  kgenhaus  23047  pthaus  23141  txhaus  23150  xkohaus  23156  haushmph  23295  cmphaushmeo  23303  hausflim  23484  hauspwpwf1  23490  hauspwpwdom  23491  hausflf  23500  cnextfun  23567  cnextfvval  23568  cnextf  23569  cnextcn  23570  cnextfres1  23571  cnextfres  23572  qtophaus  32811  ismntop  33001  poimirlem30  36513  hausgraph  41944