Metamath Proof Explorer


Theorem indistop

Description: The indiscrete topology on a set A . Part of Example 2 in Munkres p. 77. (Contributed by FL, 16-Jul-2006) (Revised by Stefan Allan, 6-Nov-2008) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion indistop
|- { (/) , A } e. Top

Proof

Step Hyp Ref Expression
1 indislem
 |-  { (/) , ( _I ` A ) } = { (/) , A }
2 fvex
 |-  ( _I ` A ) e. _V
3 indistopon
 |-  ( ( _I ` A ) e. _V -> { (/) , ( _I ` A ) } e. ( TopOn ` ( _I ` A ) ) )
4 2 3 ax-mp
 |-  { (/) , ( _I ` A ) } e. ( TopOn ` ( _I ` A ) )
5 4 topontopi
 |-  { (/) , ( _I ` A ) } e. Top
6 1 5 eqeltrri
 |-  { (/) , A } e. Top