This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) (Revised by AV, 31-Oct-2024) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses indistpsALT.a ⊢ A ∈ V
indistpsALT.k ⊢ K = Base ndx A TopSet ⁡ ndx ∅ A
Assertion indistpsALT ⊢ K ∈ TopSp

Proof

Step Hyp Ref Expression
1 indistpsALT.a ⊢ A ∈ V
2 indistpsALT.k ⊢ K = Base ndx A TopSet ⁡ ndx ∅ A
3 indistopon ⊢ A ∈ V → ∅ A ∈ TopOn ⁡ A
4 basendxlttsetndx ⊢ Base ndx < TopSet ⁡ ndx
5 tsetndxnn ⊢ TopSet ⁡ ndx ∈ ℕ
6 2 4 5 2strbas ⊢ A ∈ V → A = Base K
7 1 6 ax-mp ⊢ A = Base K
8 prex ⊢ ∅ A ∈ V
9 tsetid ⊢ TopSet = Slot TopSet ⁡ ndx
10 2 4 5 9 2strop ⊢ ∅ A ∈ V → ∅ A = TopSet ⁡ K
11 8 10 ax-mp ⊢ ∅ A = TopSet ⁡ K
12 7 11 tsettps ⊢ ∅ A ∈ TopOn ⁡ A → K ∈ TopSp
13 1 3 12 mp2b ⊢ K ∈ TopSp