**Description:** The indiscrete topology on a set A expressed as a topological space,
using explicit structure component references. Compare with indistps and indistps2 . The advantage of this version is that the actual
function for the structure is evident, and df-ndx is not needed, nor
any other special definition outside of basic set theory. The
disadvantage is that if the indices of the component definitions
df-base and df-tset are changed in the future, this theorem will
also have to be changed. Note: This theorem has hard-coded structure
indices for demonstration purposes. It is not intended for general use;
use indistps instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006)

Ref | Expression | ||
---|---|---|---|

Hypotheses | indistpsx.a | ⊢ 𝐴 ∈ V | |

indistpsx.k | ⊢ 𝐾 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 9 , { ∅ , 𝐴 } ⟩ } | ||

Assertion | indistpsx | ⊢ 𝐾 ∈ TopSp |

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

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

2 | indistpsx.k | ⊢ 𝐾 = { ⟨ 1 , 𝐴 ⟩ , ⟨ 9 , { ∅ , 𝐴 } ⟩ } | |

3 | basendx | ⊢ ( Base ‘ ndx ) = 1 | |

4 | 3 | opeq1i | ⊢ ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ = ⟨ 1 , 𝐴 ⟩ |

5 | tsetndx | ⊢ ( TopSet ‘ ndx ) = 9 | |

6 | 5 | opeq1i | ⊢ ⟨ ( TopSet ‘ ndx ) , { ∅ , 𝐴 } ⟩ = ⟨ 9 , { ∅ , 𝐴 } ⟩ |

7 | 4 6 | preq12i | ⊢ { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , { ∅ , 𝐴 } ⟩ } = { ⟨ 1 , 𝐴 ⟩ , ⟨ 9 , { ∅ , 𝐴 } ⟩ } |

8 | 2 7 | eqtr4i | ⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , { ∅ , 𝐴 } ⟩ } |

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

10 | 1 9 | ax-mp | ⊢ { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) |

11 | 10 | toponunii | ⊢ 𝐴 = ∪ { ∅ , 𝐴 } |

12 | indistop | ⊢ { ∅ , 𝐴 } ∈ Top | |

13 | 8 11 12 | eltpsi | ⊢ 𝐾 ∈ TopSp |