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 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 basendxlttsetndx 
 |-  ( Base ` ndx ) < ( TopSet ` ndx )
5 tsetndxnn 
 |-  ( TopSet ` ndx ) e. NN
6 2 4 5 2strbas 
 |-  ( A e. _V -> A = ( Base ` K ) )
7 1 6 ax-mp 
 |-  A = ( Base ` K )
8 prex 
 |-  { (/) , A } e. _V
9 tsetid 
 |-  TopSet = Slot ( TopSet ` ndx )
10 2 4 5 9 2strop 
 |-  ( { (/) , A } e. _V -> { (/) , A } = ( TopSet ` K ) )
11 8 10 ax-mp 
 |-  { (/) , A } = ( TopSet ` K )
12 7 11 tsettps 
 |-  ( { (/) , A } e. ( TopOn ` A ) -> K e. TopSp )
13 1 3 12 mp2b 
 |-  K e. TopSp