# Metamath Proof Explorer

## Theorem indistps

Description: The indiscrete topology on a set A expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx is that it is independent of the indices of the component definitions df-base and df-tset , and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 is that it is easy to eliminate the hypotheses with eqid and vtoclg to result in a closed theorem. Theorems indistpsALT and indistps2ALT show that the two forms can be derived from each other. (Contributed by FL, 19-Jul-2006)

Ref Expression
Hypotheses indistps.a 𝐴 ∈ V
indistps.k 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , { ∅ , 𝐴 } ⟩ }
Assertion indistps 𝐾 ∈ TopSp

### Proof

Step Hyp Ref Expression
1 indistps.a 𝐴 ∈ V
2 indistps.k 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , { ∅ , 𝐴 } ⟩ }
3 0ex ∅ ∈ V
4 3 1 unipr { ∅ , 𝐴 } = ( ∅ ∪ 𝐴 )
5 uncom ( ∅ ∪ 𝐴 ) = ( 𝐴 ∪ ∅ )
6 un0 ( 𝐴 ∪ ∅ ) = 𝐴
7 4 5 6 3eqtrri 𝐴 = { ∅ , 𝐴 }
8 indistop { ∅ , 𝐴 } ∈ Top
9 2 7 8 eltpsi 𝐾 ∈ TopSp