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
|- A e. _V
indistpsALT.k
|- K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , { (/) , A } >. }
Assertion indistpsALT
|- K e. TopSp

Proof

Step Hyp Ref Expression
1 indistpsALT.a
 |-  A e. _V
2 indistpsALT.k
 |-  K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , { (/) , A } >. }
3 indistopon
 |-  ( A e. _V -> { (/) , A } e. ( TopOn ` A ) )
4 df-tset
 |-  TopSet = Slot 9
5 1lt9
 |-  1 < 9
6 9nn
 |-  9 e. NN
7 2 4 5 6 2strbas
 |-  ( A e. _V -> A = ( Base ` K ) )
8 1 7 ax-mp
 |-  A = ( Base ` K )
9 prex
 |-  { (/) , A } e. _V
10 2 4 5 6 2strop
 |-  ( { (/) , A } e. _V -> { (/) , A } = ( TopSet ` K ) )
11 9 10 ax-mp
 |-  { (/) , A } = ( TopSet ` K )
12 8 11 tsettps
 |-  ( { (/) , A } e. ( TopOn ` A ) -> K e. TopSp )
13 1 3 12 mp2b
 |-  K e. TopSp