# Metamath Proof Explorer

## Theorem indistpsx

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

### Proof

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