Description: The indiscrete topology on a set A expressed as a topological space. Here we show how to derive the structural version indistps from the direct component assignment version indistps2 . (Contributed by NM, 24-Oct-2012) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | indistpsALT.a | |- A e. _V |
|
indistpsALT.k | |- K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , { (/) , A } >. } |
||
Assertion | indistpsALT | |- K e. TopSp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | indistpsALT.a | |- A e. _V |
|
2 | indistpsALT.k | |- K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , { (/) , A } >. } |
|
3 | indistopon | |- ( A e. _V -> { (/) , A } e. ( TopOn ` A ) ) |
|
4 | df-tset | |- TopSet = Slot 9 |
|
5 | 1lt9 | |- 1 < 9 |
|
6 | 9nn | |- 9 e. NN |
|
7 | 2 4 5 6 | 2strbas | |- ( A e. _V -> A = ( Base ` K ) ) |
8 | 1 7 | ax-mp | |- A = ( Base ` K ) |
9 | prex | |- { (/) , A } e. _V |
|
10 | 2 4 5 6 | 2strop | |- ( { (/) , A } e. _V -> { (/) , A } = ( TopSet ` K ) ) |
11 | 9 10 | ax-mp | |- { (/) , A } = ( TopSet ` K ) |
12 | 8 11 | tsettps | |- ( { (/) , A } e. ( TopOn ` A ) -> K e. TopSp ) |
13 | 1 3 12 | mp2b | |- K e. TopSp |