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