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

Theorem distop 17563
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 4122 . . . . . 6
2 unipw 4549 . . . . . 6
31, 2syl6sseq 3427 . . . . 5
4 vex 3009 . . . . . . 7
54uniex 6342 . . . . . 6
65elpw 3884 . . . . 5
73, 6sylibr 205 . . . 4
87ax-gen 1562 . . 3
98a1i 11 . 2
10 selpw 3885 . . . . . 6
11 selpw 3885 . . . . . . . 8
12 ssinss1 3601 . . . . . . . . . 10
1312a1i 11 . . . . . . . . 9
14 vex 3009 . . . . . . . . . . 11
1514inex2 4444 . . . . . . . . . 10
1615elpw 3884 . . . . . . . . 9
1713, 16syl6ibr 220 . . . . . . . 8
1811, 17sylbi 189 . . . . . . 7
1918com12 30 . . . . . 6
2010, 19sylbi 189 . . . . 5
2120ralrimiv 2834 . . . 4
2221rgen 2817 . . 3
2322a1i 11 . 2
24 pwexg 4483 . . 3
25 istopg 17471 . . 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 1556  e.wcel 1724  A.wral 2751   cvv 3006  i^icin 3352  C_wss 3353  ~Pcpw 3878  U.cuni 4101   ctop 17461
This theorem is referenced by:  distopon  17564  distps  17582  discld  17656  restdis  17745  dishaus  17949  discmp  17964  dis2ndc  18027  dislly  18064  dis1stc  18066  txdis  18168  xkopt  18191  xkofvcn  18220  symgtgp  18635  locfindis  27248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-8 1726  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pow 4477  ax-pr 4538  ax-un 6338
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-ral 2756  df-rex 2757  df-v 3008  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-nul 3661  df-pw 3880  df-sn 3900  df-pr 3901  df-uni 4102  df-top 17466
  Copyright terms: Public domain W3C validator