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

Metamath Proof Explorer

Theorem indistps2

Description: The indiscrete topology on a set A expressed as a topological space, using direct component assignments. Compare with indistps . The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT and indistps2ALT show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012)

Ref Expression
Hypotheses indistps2.a ⊢ ( Base ‘ 𝐾 ) = 𝐴
indistps2.j ⊢ ( TopOpen ‘ 𝐾 ) = { ∅ , 𝐴 }
Assertion indistps2 𝐾 ∈ TopSp

Proof

Step Hyp Ref Expression
1 indistps2.a ⊢ ( Base ‘ 𝐾 ) = 𝐴
2 indistps2.j ⊢ ( TopOpen ‘ 𝐾 ) = { ∅ , 𝐴 }
3 0ex ⊢ ∅ ∈ V
4 fvex ⊢ ( Base ‘ 𝐾 ) ∈ V
5 1 4 eqeltrri ⊢ 𝐴 ∈ V
6 3 5 unipr ⊢ ∪ { ∅ , 𝐴 } = ( ∅ ∪ 𝐴 )
7 uncom ⊢ ( ∅ ∪ 𝐴 ) = ( 𝐴 ∪ ∅ )
8 un0 ⊢ ( 𝐴 ∪ ∅ ) = 𝐴
9 6 7 8 3eqtrri ⊢ 𝐴 = ∪ { ∅ , 𝐴 }
10 indistop ⊢ { ∅ , 𝐴 } ∈ Top
11 1 2 9 10 istpsi ⊢ 𝐾 ∈ TopSp