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

Theorem distop 18074
Description: The discrete topology on a set . 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

Proof of Theorem distop
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uniss 4138 . . . . . 6
2 unipw 4565 . . . . . 6
31, 2syl6sseq 3439 . . . . 5
4 vex 3018 . . . . . . 7
54uniex 6386 . . . . . 6
65elpw 3899 . . . . 5
73, 6sylibr 205 . . . 4
87ax-gen 1570 . . 3
98a1i 11 . 2
10 selpw 3900 . . . . . 6
11 selpw 3900 . . . . . . . 8
12 ssinss1 3614 . . . . . . . . . 10
1312a1i 11 . . . . . . . . 9
14 vex 3018 . . . . . . . . . . 11
1514inex2 4460 . . . . . . . . . 10
1615elpw 3899 . . . . . . . . 9
1713, 16syl6ibr 220 . . . . . . . 8
1811, 17sylbi 189 . . . . . . 7
1918com12 30 . . . . . 6
2010, 19sylbi 189 . . . . 5
2120ralrimiv 2842 . . . 4
2221rgen 2825 . . 3
2322a1i 11 . 2
24 pwexg 4499 . . 3
25 istopg 17982 . . 3
2624, 25syl 16 . 2
279, 23, 26mpbir2and 890 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  /\wa 360  A.wal 1564  e.wcel 1732  A.wral 2759   cvv 3015  i^icin 3364  C_wss 3365  ~Pcpw 3893  U.cuni 4117   ctop 17972
This theorem is referenced by:  distopon  18075  distps  18093  discld  18167  restdis  18256  dishaus  18460  discmp  18475  dis2ndc  18538  dislly  18575  dis1stc  18577  txdis  18679  xkopt  18702  xkofvcn  18731  symgtgp  19146  locfindis  27757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-v 3017  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-pw 3895  df-sn 3915  df-pr 3916  df-uni 4118  df-top 17977
  Copyright terms: Public domain W3C validator