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

Theorem distop 16729
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
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uniss 3849 . . . . . 6  |-  ( x 
C_  ~P A  ->  U. x  C_ 
U. ~P A )
2 unipw 4223 . . . . . 6  |-  U. ~P A  =  A
31, 2syl6sseq 3225 . . . . 5  |-  ( x 
C_  ~P A  ->  U. x  C_  A )
4 vex 2792 . . . . . . 7  |-  x  e. 
_V
54uniex 4515 . . . . . 6  |-  U. x  e.  _V
65elpw 3632 . . . . 5  |-  ( U. x  e.  ~P A  <->  U. x  C_  A )
73, 6sylibr 203 . . . 4  |-  ( x 
C_  ~P A  ->  U. x  e.  ~P A )
87ax-gen 1533 . . 3  |-  A. x
( x  C_  ~P A  ->  U. x  e.  ~P A )
98a1i 10 . 2  |-  ( A  e.  V  ->  A. x
( x  C_  ~P A  ->  U. x  e.  ~P A ) )
104elpw 3632 . . . . . 6  |-  ( x  e.  ~P A  <->  x  C_  A
)
11 vex 2792 . . . . . . . . 9  |-  y  e. 
_V
1211elpw 3632 . . . . . . . 8  |-  ( y  e.  ~P A  <->  y  C_  A )
13 ssinss1 3398 . . . . . . . . . 10  |-  ( x 
C_  A  ->  (
x  i^i  y )  C_  A )
1413a1i 10 . . . . . . . . 9  |-  ( y 
C_  A  ->  (
x  C_  A  ->  ( x  i^i  y ) 
C_  A ) )
1511inex2 4157 . . . . . . . . . 10  |-  ( x  i^i  y )  e. 
_V
1615elpw 3632 . . . . . . . . 9  |-  ( ( x  i^i  y )  e.  ~P A  <->  ( x  i^i  y )  C_  A
)
1714, 16syl6ibr 218 . . . . . . . 8  |-  ( y 
C_  A  ->  (
x  C_  A  ->  ( x  i^i  y )  e.  ~P A ) )
1812, 17sylbi 187 . . . . . . 7  |-  ( y  e.  ~P A  -> 
( x  C_  A  ->  ( x  i^i  y
)  e.  ~P A
) )
1918com12 27 . . . . . 6  |-  ( x 
C_  A  ->  (
y  e.  ~P A  ->  ( x  i^i  y
)  e.  ~P A
) )
2010, 19sylbi 187 . . . . 5  |-  ( x  e.  ~P A  -> 
( y  e.  ~P A  ->  ( x  i^i  y )  e.  ~P A ) )
2120ralrimiv 2626 . . . 4  |-  ( x  e.  ~P A  ->  A. y  e.  ~P  A ( x  i^i  y )  e.  ~P A )
2221rgen 2609 . . 3  |-  A. x  e.  ~P  A A. y  e.  ~P  A ( x  i^i  y )  e. 
~P A
2322a1i 10 . 2  |-  ( A  e.  V  ->  A. x  e.  ~P  A A. y  e.  ~P  A ( x  i^i  y )  e. 
~P A )
24 pwexg 4193 . . 3  |-  ( A  e.  V  ->  ~P A  e.  _V )
25 istopg 16637 . . 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 15 . 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 888 1  |-  ( A  e.  V  ->  ~P A  e.  Top )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527    e. wcel 1685   A.wral 2544   _Vcvv 2789    i^i cin 3152    C_ wss 3153   ~Pcpw 3626   U.cuni 3828   Topctop 16627
This theorem is referenced by:  distopon  16730  distps  16748  discld  16822  restdis  16905  dishaus  17106  discmp  17121  dis2ndc  17182  dislly  17219  dis1stc  17221  txdis  17322  xkopt  17345  xkofvcn  17374  symgtgp  17780  usptoplem  24957  istopx  24958  locfindis  25716
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-pw 3628  df-sn 3647  df-pr 3648  df-uni 3829  df-top 16632
  Copyright terms: Public domain W3C validator