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 2821 | . . 3 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
2 | 1 | ishaus 21924 | . 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) |
3 | 2 | simplbi 500 | 1 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 ∩ cin 3935 ∅c0 4291 ∪ cuni 4832 Topctop 21495 Hauscha 21910 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-uni 4833 df-haus 21917 |
This theorem is referenced by: haust1 21954 resthaus 21970 sshaus 21977 lmmo 21982 hauscmplem 22008 hauscmp 22009 hauslly 22094 hausllycmp 22096 kgenhaus 22146 pthaus 22240 txhaus 22249 xkohaus 22255 haushmph 22394 cmphaushmeo 22402 hausflim 22583 hauspwpwf1 22589 hauspwpwdom 22590 hausflf 22599 cnextfun 22666 cnextfvval 22667 cnextf 22668 cnextcn 22669 cnextfres1 22670 cnextfres 22671 qtophaus 31095 ismntop 31262 poimirlem30 34916 hausgraph 39805 |
Copyright terms: Public domain | W3C validator |