Metamath Proof Explorer


Theorem distopon

Description: The discrete topology on a set A , with base set. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion distopon
|- ( A e. V -> ~P A e. ( TopOn ` A ) )

Proof

Step Hyp Ref Expression
1 distop
 |-  ( A e. V -> ~P A e. Top )
2 unipw
 |-  U. ~P A = A
3 2 eqcomi
 |-  A = U. ~P A
4 istopon
 |-  ( ~P A e. ( TopOn ` A ) <-> ( ~P A e. Top /\ A = U. ~P A ) )
5 1 3 4 sylanblrc
 |-  ( A e. V -> ~P A e. ( TopOn ` A ) )