Description: Obsolete proof of indistpsALT as of 31-Oct-2024. 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 | indistpsALTOLD | |- 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 |