MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  distop Unicode version

Theorem distop 16696
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.)
Assertion
Ref Expression
distop  |-  ( A  e.  V  ->  ~P A  e.  Top )

Proof of Theorem distop
StepHypRef Expression
1 uniss 3822 . . . . . 6  |-  ( x 
C_  ~P A  ->  U. x  C_ 
U. ~P A )
2 unipw 4196 . . . . . 6  |-  U. ~P A  =  A
31, 2syl6sseq 3199 . . . . 5  |-  ( x 
C_  ~P A  ->  U. x  C_  A )
4 vex 2766 . . . . . . 7  |-  x  e. 
_V
54uniex 4488 . . . . . 6  |-  U. x  e.  _V
65elpw 3605 . . . . 5  |-  ( U. x  e.  ~P A  <->  U. x  C_  A )
73, 6sylibr 205 . . . 4  |-  ( x 
C_  ~P A  ->  U. x  e.  ~P A )
87ax-gen 1536 . . 3  |-  A. x
( x  C_  ~P A  ->  U. x  e.  ~P A )
98a1i 12 . 2  |-  ( A  e.  V  ->  A. x
( x  C_  ~P A  ->  U. x  e.  ~P A ) )
104elpw 3605 . . . . . 6  |-  ( x  e.  ~P A  <->  x  C_  A
)
11 vex 2766 . . . . . . . . 9  |-  y  e. 
_V
1211elpw 3605 . . . . . . . 8  |-  ( y  e.  ~P A  <->  y  C_  A )
13 ssinss1 3372 . . . . . . . . . 10  |-  ( x 
C_  A  ->  (
x  i^i  y )  C_  A )
1413a1i 12 . . . . . . . . 9  |-  ( y 
C_  A  ->  (
x  C_  A  ->  ( x  i^i  y ) 
C_  A ) )
1511inex2 4130 . . . . . . . . . 10  |-  ( x  i^i  y )  e. 
_V
1615elpw 3605 . . . . . . . . 9  |-  ( ( x  i^i  y )  e.  ~P A  <->  ( x  i^i  y )  C_  A
)
1714, 16syl6ibr 220 . . . . . . . 8  |-  ( y 
C_  A  ->  (
x  C_  A  ->  ( x  i^i  y )  e.  ~P A ) )
1812, 17sylbi 189 . . . . . . 7  |-  ( y  e.  ~P A  -> 
( x  C_  A  ->  ( x  i^i  y
)  e.  ~P A
) )
1918com12 29 . . . . . 6  |-  ( x 
C_  A  ->  (
y  e.  ~P A  ->  ( x  i^i  y
)  e.  ~P A
) )
2010, 19sylbi 189 . . . . 5  |-  ( x  e.  ~P A  -> 
( y  e.  ~P A  ->  ( x  i^i  y )  e.  ~P A ) )
2120ralrimiv 2600 . . . 4  |-  ( x  e.  ~P A  ->  A. y  e.  ~P  A ( x  i^i  y )  e.  ~P A )
2221rgen 2583 . . 3  |-  A. x  e.  ~P  A A. y  e.  ~P  A ( x  i^i  y )  e. 
~P A
2322a1i 12 . 2  |-  ( A  e.  V  ->  A. x  e.  ~P  A A. y  e.  ~P  A ( x  i^i  y )  e. 
~P A )
24 pwexg 4166 . . 3  |-  ( A  e.  V  ->  ~P A  e.  _V )
25 istopg 16604 . . 3  |-  ( ~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 ) ) )
2624, 25syl 17 . 2  |-  ( 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 ) ) )
279, 23, 26mpbir2and 893 1  |-  ( A  e.  V  ->  ~P A  e.  Top )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360   A.wal 1532    e. wcel 1621   A.wral 2518   _Vcvv 2763    i^i cin 3126    C_ wss 3127   ~Pcpw 3599   U.cuni 3801   Topctop 16594
This theorem is referenced by:  distopon  16697  distps  16715  discld  16789  restdis  16872  dishaus  17073  discmp  17088  dis2ndc  17149  dislly  17186  dis1stc  17188  txdis  17289  xkopt  17312  xkofvcn  17341  symgtgp  17747  usptoplem  24914  istopx  24915  locfindis  25673
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pow 4160  ax-pr 4186  ax-un 4484
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-pw 3601  df-sn 3620  df-pr 3621  df-uni 3802  df-top 16599
  Copyright terms: Public domain W3C validator