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

Theorem istopon 18630
Description: Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 13-Aug-2015.)
Assertion
Ref Expression
istopon

Proof of Theorem istopon
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfvex 5800 . 2
2 uniexg 6461 . . . 4
3 eleq1 2520 . . . 4
42, 3syl5ibrcom 222 . . 3
54imp 429 . 2
6 eqeq1 2453 . . . . . 6
76rabbidv 3044 . . . . 5
8 df-topon 18606 . . . . 5
9 vex 3055 . . . . . . . 8
109pwex 4557 . . . . . . 7
1110pwex 4557 . . . . . 6
12 rabss 3511 . . . . . . 7
13 pwuni 4605 . . . . . . . . . 10
14 pweq 3945 . . . . . . . . . 10
1513, 14syl5sseqr 3487 . . . . . . . . 9
16 selpw 3949 . . . . . . . . 9
1715, 16sylibr 212 . . . . . . . 8
1817a1i 11 . . . . . . 7
1912, 18mprgbir 2865 . . . . . 6
2011, 19ssexi 4519 . . . . 5
217, 8, 20fvmpt3i 5861 . . . 4
2221eleq2d 2519 . . 3
23 unieq 4181 . . . . 5
2423eqeq2d 2463 . . . 4
2524elrab 3198 . . 3
2622, 25syl6bb 261 . 2
271, 5, 26pm5.21nii 353 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1370  e.wcel 1757  {crab 2796   cvv 3052  C_wss 3410  ~Pcpw 3942  U.cuni 4173  `cfv 5500   ctop 18598   ctopon 18599
This theorem is referenced by:  topontop  18631  toponuni  18632  toponcom  18635  toptopon  18638  istps2  18642  tgtopon  18676  distopon  18701  indistopon  18705  fctop  18708  cctop  18710  ppttop  18711  epttop  18713  mretopd  18796  toponmre  18797  resttopon  18865  resttopon2  18872  kgentopon  19211  txtopon  19264  pttopon  19269  xkotopon  19273  qtoptopon  19377  flimtopon  19643  fclstopon  19685  fclsfnflim  19700  utoptopon  19911  onsuctopon  28398  neibastop1  28702  rfcnpre1  29863  cnfex  29872  stoweidlem47  29964
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3054  df-sbc 3269  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4174  df-br 4375  df-opab 4433  df-mpt 4434  df-id 4718  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-iota 5463  df-fun 5502  df-fv 5508  df-topon 18606
  Copyright terms: Public domain W3C validator