**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 | ⊢ 𝐴 ∈ V | |

indistpsALT.k | ⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , { ∅ , 𝐴 } ⟩ } | ||

Assertion | indistpsALT | ⊢ 𝐾 ∈ TopSp |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | indistpsALT.a | ⊢ 𝐴 ∈ V | |

2 | indistpsALT.k | ⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , { ∅ , 𝐴 } ⟩ } | |

3 | indistopon | ⊢ ( 𝐴 ∈ V → { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) ) | |

4 | df-tset | ⊢ TopSet = Slot 9 | |

5 | 1lt9 | ⊢ 1 < 9 | |

6 | 9nn | ⊢ 9 ∈ ℕ | |

7 | 2 4 5 6 | 2strbas | ⊢ ( 𝐴 ∈ V → 𝐴 = ( Base ‘ 𝐾 ) ) |

8 | 1 7 | ax-mp | ⊢ 𝐴 = ( Base ‘ 𝐾 ) |

9 | prex | ⊢ { ∅ , 𝐴 } ∈ V | |

10 | 2 4 5 6 | 2strop | ⊢ ( { ∅ , 𝐴 } ∈ V → { ∅ , 𝐴 } = ( TopSet ‘ 𝐾 ) ) |

11 | 9 10 | ax-mp | ⊢ { ∅ , 𝐴 } = ( TopSet ‘ 𝐾 ) |

12 | 8 11 | tsettps | ⊢ ( { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ TopSp ) |

13 | 1 3 12 | mp2b | ⊢ 𝐾 ∈ TopSp |