Description: The indiscrete topology on a set A . Part of Example 2 in Munkres p. 77. (Contributed by FL, 16-Jul-2006) (Revised by Stefan Allan, 6-Nov-2008) (Revised by Mario Carneiro, 13-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | indistop | |- { (/) , A } e. Top |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | indislem | |- { (/) , ( _I ` A ) } = { (/) , A } |
|
| 2 | fvex | |- ( _I ` A ) e. _V |
|
| 3 | indistopon | |- ( ( _I ` A ) e. _V -> { (/) , ( _I ` A ) } e. ( TopOn ` ( _I ` A ) ) ) |
|
| 4 | 2 3 | ax-mp | |- { (/) , ( _I ` A ) } e. ( TopOn ` ( _I ` A ) ) |
| 5 | 4 | topontopi | |- { (/) , ( _I ` A ) } e. Top |
| 6 | 1 5 | eqeltrri | |- { (/) , A } e. Top |