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 |