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

Theorem istopon 19940
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 5892 . 2  |-  ( J  e.  (TopOn `  B
)  ->  B  e.  _V )
2 uniexg 6588 . . . 4  |-  ( J  e.  Top  ->  U. J  e.  _V )
3 eleq1 2517 . . . 4  |-  ( B  =  U. J  -> 
( B  e.  _V  <->  U. J  e.  _V )
)
42, 3syl5ibrcom 226 . . 3  |-  ( J  e.  Top  ->  ( B  =  U. J  ->  B  e.  _V )
)
54imp 431 . 2  |-  ( ( J  e.  Top  /\  B  =  U. J )  ->  B  e.  _V )
6 eqeq1 2455 . . . . . 6  |-  ( b  =  B  ->  (
b  =  U. j  <->  B  =  U. j ) )
76rabbidv 3036 . . . . 5  |-  ( b  =  B  ->  { j  e.  Top  |  b  =  U. j }  =  { j  e. 
Top  |  B  =  U. j } )
8 df-topon 19923 . . . . 5  |- TopOn  =  ( b  e.  _V  |->  { j  e.  Top  | 
b  =  U. j } )
9 vex 3048 . . . . . . . 8  |-  b  e. 
_V
109pwex 4586 . . . . . . 7  |-  ~P b  e.  _V
1110pwex 4586 . . . . . 6  |-  ~P ~P b  e.  _V
12 rabss 3506 . . . . . . 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 3954 . . . . . . . . . 10  |-  ( b  =  U. j  ->  ~P b  =  ~P U. j )
1513, 14syl5sseqr 3481 . . . . . . . . 9  |-  ( b  =  U. j  -> 
j  C_  ~P b
)
16 selpw 3958 . . . . . . . . 9  |-  ( j  e.  ~P ~P b  <->  j 
C_  ~P b )
1715, 16sylibr 216 . . . . . . . 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 2752 . . . . . 6  |-  { j  e.  Top  |  b  =  U. j } 
C_  ~P ~P b
2011, 19ssexi 4548 . . . . 5  |-  { j  e.  Top  |  b  =  U. j }  e.  _V
217, 8, 20fvmpt3i 5953 . . . 4  |-  ( B  e.  _V  ->  (TopOn `  B )  =  {
j  e.  Top  |  B  =  U. j } )
2221eleq2d 2514 . . 3  |-  ( B  e.  _V  ->  ( J  e.  (TopOn `  B
)  <->  J  e.  { j  e.  Top  |  B  =  U. j } ) )
23 unieq 4206 . . . . 5  |-  ( j  =  J  ->  U. j  =  U. J )
2423eqeq2d 2461 . . . 4  |-  ( j  =  J  ->  ( B  =  U. j  <->  B  =  U. J ) )
2524elrab 3196 . . 3  |-  ( J  e.  { j  e. 
Top  |  B  =  U. j }  <->  ( J  e.  Top  /\  B  = 
U. J ) )
2622, 25syl6bb 265 . 2  |-  ( B  e.  _V  ->  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) ) )
271, 5, 26pm5.21nii 355 1  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1444    e. wcel 1887   {crab 2741   _Vcvv 3045    C_ wss 3404   ~Pcpw 3951   U.cuni 4198   ` cfv 5582   Topctop 19917  TopOnctopon 19918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-iota 5546  df-fun 5584  df-fv 5590  df-topon 19923
This theorem is referenced by:  topontop  19941  toponuni  19942  toponcom  19945  toptopon  19948  istps2  19952  tgtopon  19987  distopon  20012  indistopon  20016  fctop  20019  cctop  20021  ppttop  20022  epttop  20024  mretopd  20108  toponmre  20109  resttopon  20177  resttopon2  20184  kgentopon  20553  txtopon  20606  pttopon  20611  xkotopon  20615  qtoptopon  20719  flimtopon  20985  fclstopon  21027  fclsfnflim  21042  utoptopon  21251  qtopt1  28662  neibastop1  31015  onsuctopon  31094  rfcnpre1  37340  cnfex  37349  icccncfext  37765  stoweidlem47  37908
  Copyright terms: Public domain W3C validator