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

Theorem distop 16735
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 3850 . . . . . 6  |-  ( x 
C_  ~P A  ->  U. x  C_ 
U. ~P A )
2 unipw 4226 . . . . . 6  |-  U. ~P A  =  A
31, 2syl6sseq 3226 . . . . 5  |-  ( x 
C_  ~P A  ->  U. x  C_  A )
4 vex 2793 . . . . . . 7  |-  x  e. 
_V
54uniex 4518 . . . . . 6  |-  U. x  e.  _V
65elpw 3633 . . . . 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 1535 . . 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 3633 . . . . . 6  |-  ( x  e.  ~P A  <->  x  C_  A
)
11 vex 2793 . . . . . . . . 9  |-  y  e. 
_V
1211elpw 3633 . . . . . . . 8  |-  ( y  e.  ~P A  <->  y  C_  A )
13 ssinss1 3399 . . . . . . . . . 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 4158 . . . . . . . . . 10  |-  ( x  i^i  y )  e. 
_V
1615elpw 3633 . . . . . . . . 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 2627 . . . 4  |-  ( x  e.  ~P A  ->  A. y  e.  ~P  A ( x  i^i  y )  e.  ~P A )
2221rgen 2610 . . 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 4196 . . 3  |-  ( A  e.  V  ->  ~P A  e.  _V )
25 istopg 16643 . . 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 1529    e. wcel 1686   A.wral 2545   _Vcvv 2790    i^i cin 3153    C_ wss 3154   ~Pcpw 3627   U.cuni 3829   Topctop 16633
This theorem is referenced by:  distopon  16736  distps  16754  discld  16828  restdis  16911  dishaus  17112  discmp  17127  dis2ndc  17188  dislly  17225  dis1stc  17227  txdis  17328  xkopt  17351  xkofvcn  17380  symgtgp  17786  usptoplem  25557  istopx  25558  locfindis  26316
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-pw 3629  df-sn 3648  df-pr 3649  df-uni 3830  df-top 16638
  Copyright terms: Public domain W3C validator