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 ) )