Metamath Proof Explorer


Theorem distop

Description: The discrete topology on a set A . Part of Example 2 in Munkres p. 77. (Contributed by FL, 17-Jul-2006) (Revised by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion distop
|- ( A e. V -> ~P A e. Top )

Proof

Step Hyp Ref Expression
1 uniss
 |-  ( x C_ ~P A -> U. x C_ U. ~P A )
2 unipw
 |-  U. ~P A = A
3 1 2 sseqtrdi
 |-  ( x C_ ~P A -> U. x C_ A )
4 vuniex
 |-  U. x e. _V
5 4 elpw
 |-  ( U. x e. ~P A <-> U. x C_ A )
6 3 5 sylibr
 |-  ( x C_ ~P A -> U. x e. ~P A )
7 6 ax-gen
 |-  A. x ( x C_ ~P A -> U. x e. ~P A )
8 7 a1i
 |-  ( A e. V -> A. x ( x C_ ~P A -> U. x e. ~P A ) )
9 velpw
 |-  ( x e. ~P A <-> x C_ A )
10 velpw
 |-  ( y e. ~P A <-> y C_ A )
11 ssinss1
 |-  ( x C_ A -> ( x i^i y ) C_ A )
12 11 a1i
 |-  ( y C_ A -> ( x C_ A -> ( x i^i y ) C_ A ) )
13 vex
 |-  y e. _V
14 13 inex2
 |-  ( x i^i y ) e. _V
15 14 elpw
 |-  ( ( x i^i y ) e. ~P A <-> ( x i^i y ) C_ A )
16 12 15 syl6ibr
 |-  ( y C_ A -> ( x C_ A -> ( x i^i y ) e. ~P A ) )
17 10 16 sylbi
 |-  ( y e. ~P A -> ( x C_ A -> ( x i^i y ) e. ~P A ) )
18 17 com12
 |-  ( x C_ A -> ( y e. ~P A -> ( x i^i y ) e. ~P A ) )
19 9 18 sylbi
 |-  ( x e. ~P A -> ( y e. ~P A -> ( x i^i y ) e. ~P A ) )
20 19 ralrimiv
 |-  ( x e. ~P A -> A. y e. ~P A ( x i^i y ) e. ~P A )
21 20 rgen
 |-  A. x e. ~P A A. y e. ~P A ( x i^i y ) e. ~P A
22 21 a1i
 |-  ( A e. V -> A. x e. ~P A A. y e. ~P A ( x i^i y ) e. ~P A )
23 pwexg
 |-  ( A e. V -> ~P A e. _V )
24 istopg
 |-  ( ~P A e. _V -> ( ~P A e. Top <-> ( A. x ( x C_ ~P A -> U. x e. ~P A ) /\ A. x e. ~P A A. y e. ~P A ( x i^i y ) e. ~P A ) ) )
25 23 24 syl
 |-  ( A e. V -> ( ~P A e. Top <-> ( A. x ( x C_ ~P A -> U. x e. ~P A ) /\ A. x e. ~P A A. y e. ~P A ( x i^i y ) e. ~P A ) ) )
26 8 22 25 mpbir2and
 |-  ( A e. V -> ~P A e. Top )