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 |