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

Theorem distop 17111
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 4063 . . . . . 6
2 unipw 4453 . . . . . 6
31, 2syl6sseq 3383 . . . . 5
4 vex 2968 . . . . . . 7
54uniex 4746 . . . . . 6
65elpw 3832 . . . . 5
73, 6sylibr 205 . . . 4
87ax-gen 1556 . . 3
98a1i 11 . 2
104elpw 3832 . . . . . 6
11 vex 2968 . . . . . . . . 9
1211elpw 3832 . . . . . . . 8
13 ssinss1 3557 . . . . . . . . . 10
1413a1i 11 . . . . . . . . 9
1511inex2 4384 . . . . . . . . . 10
1615elpw 3832 . . . . . . . . 9
1714, 16syl6ibr 220 . . . . . . . 8
1812, 17sylbi 189 . . . . . . 7
1918com12 30 . . . . . 6
2010, 19sylbi 189 . . . . 5
2120ralrimiv 2795 . . . 4
2221rgen 2778 . . 3
2322a1i 11 . 2
24 pwexg 4422 . . 3
25 istopg 17019 . . 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 1550  e.wcel 1728  A.wral 2712   cvv 2965  i^icin 3308  C_wss 3309  ~Pcpw 3826  U.cuni 4043   ctop 17009
This theorem is referenced by:  distopon  17112  distps  17130  discld  17204  restdis  17293  dishaus  17497  discmp  17512  dis2ndc  17574  dislly  17611  dis1stc  17613  txdis  17715  xkopt  17738  xkofvcn  17767  symgtgp  18182  locfindis  26496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4364  ax-nul 4372  ax-pow 4416  ax-pr 4442  ax-un 4742
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-v 2967  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-pw 3828  df-sn 3847  df-pr 3848  df-uni 4044  df-top 17014
  Copyright terms: Public domain W3C validator