# Metamath Proof Explorer

## Theorem indistpsALT

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

### Proof

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