This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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