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 2737 | . . 3 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
2 | 1 | ishaus 22219 | . 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) |
3 | 2 | simplbi 501 | 1 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1089 = wceq 1543 ∈ wcel 2110 ≠ wne 2940 ∀wral 3061 ∃wrex 3062 ∩ cin 3865 ∅c0 4237 ∪ cuni 4819 Topctop 21790 Hauscha 22205 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 df-in 3873 df-ss 3883 df-uni 4820 df-haus 22212 |
This theorem is referenced by: haust1 22249 resthaus 22265 sshaus 22272 lmmo 22277 hauscmplem 22303 hauscmp 22304 hauslly 22389 hausllycmp 22391 kgenhaus 22441 pthaus 22535 txhaus 22544 xkohaus 22550 haushmph 22689 cmphaushmeo 22697 hausflim 22878 hauspwpwf1 22884 hauspwpwdom 22885 hausflf 22894 cnextfun 22961 cnextfvval 22962 cnextf 22963 cnextcn 22964 cnextfres1 22965 cnextfres 22966 qtophaus 31500 ismntop 31688 poimirlem30 35544 hausgraph 40740 |
Copyright terms: Public domain | W3C validator |