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

Theorem istopon 20017
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  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )

Proof of Theorem istopon
Dummy variables  b 
j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfvex 5906 . 2  |-  ( J  e.  (TopOn `  B
)  ->  B  e.  _V )
2 uniexg 6607 . . . 4  |-  ( J  e.  Top  ->  U. J  e.  _V )
3 eleq1 2537 . . . 4  |-  ( B  =  U. J  -> 
( B  e.  _V  <->  U. J  e.  _V )
)
42, 3syl5ibrcom 230 . . 3  |-  ( J  e.  Top  ->  ( B  =  U. J  ->  B  e.  _V )
)
54imp 436 . 2  |-  ( ( J  e.  Top  /\  B  =  U. J )  ->  B  e.  _V )
6 eqeq1 2475 . . . . . 6  |-  ( b  =  B  ->  (
b  =  U. j  <->  B  =  U. j ) )
76rabbidv 3022 . . . . 5  |-  ( b  =  B  ->  { j  e.  Top  |  b  =  U. j }  =  { j  e. 
Top  |  B  =  U. j } )
8 df-topon 20000 . . . . 5  |- TopOn  =  ( b  e.  _V  |->  { j  e.  Top  | 
b  =  U. j } )
9 vex 3034 . . . . . . . 8  |-  b  e. 
_V
109pwex 4584 . . . . . . 7  |-  ~P b  e.  _V
1110pwex 4584 . . . . . 6  |-  ~P ~P b  e.  _V
12 rabss 3492 . . . . . . 7  |-  ( { j  e.  Top  | 
b  =  U. j }  C_  ~P ~P b  <->  A. j  e.  Top  (
b  =  U. j  ->  j  e.  ~P ~P b ) )
13 pwuni 4631 . . . . . . . . . 10  |-  j  C_  ~P U. j
14 pweq 3945 . . . . . . . . . 10  |-  ( b  =  U. j  ->  ~P b  =  ~P U. j )
1513, 14syl5sseqr 3467 . . . . . . . . 9  |-  ( b  =  U. j  -> 
j  C_  ~P b
)
16 selpw 3949 . . . . . . . . 9  |-  ( j  e.  ~P ~P b  <->  j 
C_  ~P b )
1715, 16sylibr 217 . . . . . . . 8  |-  ( b  =  U. j  -> 
j  e.  ~P ~P b )
1817a1i 11 . . . . . . 7  |-  ( j  e.  Top  ->  (
b  =  U. j  ->  j  e.  ~P ~P b ) )
1912, 18mprgbir 2771 . . . . . 6  |-  { j  e.  Top  |  b  =  U. j } 
C_  ~P ~P b
2011, 19ssexi 4541 . . . . 5  |-  { j  e.  Top  |  b  =  U. j }  e.  _V
217, 8, 20fvmpt3i 5968 . . . 4  |-  ( B  e.  _V  ->  (TopOn `  B )  =  {
j  e.  Top  |  B  =  U. j } )
2221eleq2d 2534 . . 3  |-  ( B  e.  _V  ->  ( J  e.  (TopOn `  B
)  <->  J  e.  { j  e.  Top  |  B  =  U. j } ) )
23 unieq 4198 . . . . 5  |-  ( j  =  J  ->  U. j  =  U. J )
2423eqeq2d 2481 . . . 4  |-  ( j  =  J  ->  ( B  =  U. j  <->  B  =  U. J ) )
2524elrab 3184 . . 3  |-  ( J  e.  { j  e. 
Top  |  B  =  U. j }  <->  ( J  e.  Top  /\  B  = 
U. J ) )
2622, 25syl6bb 269 . 2  |-  ( B  e.  _V  ->  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) ) )
271, 5, 26pm5.21nii 360 1  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376    = wceq 1452    e. wcel 1904   {crab 2760   _Vcvv 3031    C_ wss 3390   ~Pcpw 3942   U.cuni 4190   ` cfv 5589   Topctop 19994  TopOnctopon 19995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-iota 5553  df-fun 5591  df-fv 5597  df-topon 20000
This theorem is referenced by:  topontop  20018  toponuni  20019  toponcom  20022  toptopon  20025  istps2  20029  tgtopon  20064  distopon  20089  indistopon  20093  fctop  20096  cctop  20098  ppttop  20099  epttop  20101  mretopd  20185  toponmre  20186  resttopon  20254  resttopon2  20261  kgentopon  20630  txtopon  20683  pttopon  20688  xkotopon  20692  qtoptopon  20796  flimtopon  21063  fclstopon  21105  fclsfnflim  21120  utoptopon  21329  qtopt1  28736  neibastop1  31086  onsuctopon  31165  rfcnpre1  37403  cnfex  37412  icccncfext  37862  stoweidlem47  38020
  Copyright terms: Public domain W3C validator