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 ⊢ 𝐴 ∈ 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 basendxlttsetndx ⊢ ( Base ‘ ndx ) < ( TopSet ‘ ndx )
5 tsetndxnn ⊢ ( TopSet ‘ ndx ) ∈ ℕ
6 2 4 5 2strbas ⊢ ( 𝐴 ∈ V → 𝐴 = ( Base ‘ 𝐾 ) )
7 1 6 ax-mp ⊢ 𝐴 = ( Base ‘ 𝐾 )
8 prex ⊢ { ∅ , 𝐴 } ∈ V
9 tsetid ⊢ TopSet = Slot ( TopSet ‘ ndx )
10 2 4 5 9 2strop ⊢ ( { ∅ , 𝐴 } ∈ V → { ∅ , 𝐴 } = ( TopSet ‘ 𝐾 ) )
11 8 10 ax-mp ⊢ { ∅ , 𝐴 } = ( TopSet ‘ 𝐾 )
12 7 11 tsettps ⊢ ( { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ TopSp )
13 1 3 12 mp2b ⊢ 𝐾 ∈ TopSp