![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > haustop | Structured version Visualization version GIF version |
Description: A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.) |
Ref | Expression |
---|---|
haustop | ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2725 | . . 3 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
2 | 1 | ishaus 23270 | . 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) |
3 | 2 | simplbi 496 | 1 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ≠ wne 2929 ∀wral 3050 ∃wrex 3059 ∩ cin 3943 ∅c0 4322 ∪ cuni 4909 Topctop 22839 Hauscha 23256 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-ss 3961 df-uni 4910 df-haus 23263 |
This theorem is referenced by: haust1 23300 resthaus 23316 sshaus 23323 lmmo 23328 hauscmplem 23354 hauscmp 23355 hauslly 23440 hausllycmp 23442 kgenhaus 23492 pthaus 23586 txhaus 23595 xkohaus 23601 haushmph 23740 cmphaushmeo 23748 hausflim 23929 hauspwpwf1 23935 hauspwpwdom 23936 hausflf 23945 cnextfun 24012 cnextfvval 24013 cnextf 24014 cnextcn 24015 cnextfres1 24016 cnextfres 24017 qtophaus 33568 ismntop 33758 poimirlem30 37254 hausgraph 42775 |
Copyright terms: Public domain | W3C validator |