Theorem haustop 23649

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  ∃wrex 3086   ∩ cin 4089  ∅c0 4278  ∪ cuni 4866  Topctop 23211  Hauscha 23626

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-uni 4867  df-haus 23633

This theorem is used by:  haust1  23670  resthaus  23686  sshaus  23693  lmmo  23698  hauscmplem  23724  hauscmp  23725  hauslly  23811  hausllycmp  23813  kgenhaus  23863  pthaus  23957  txhaus  23966  xkohaus  23972  haushmph  24111  cmphaushmeo  24119  hausflim  24300  hauspwpwf1  24306  hauspwpwdom  24307  hausflf  24316  cnextfun  24383  cnextfvval  24384  cnextf  24385  cnextcn  24386  cnextfres1  24387  cnextfres  24388  qtophaus  34468  ismntop  34658  poimirlem30  38569  hausgraph  44207