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 ATop

Proof

Step Hyp Ref Expression
1 indislem IA=A
2 fvex IAV
3 indistopon IAVIATopOnIA
4 2 3 ax-mp IATopOnIA
5 4 topontopi IATop
6 1 5 eqeltrri ATop