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

Definition df-pt 13345
Description: Define the product topology on a collection of topologies. For convenience, it is defined on arbitrary collections of sets, expressed as a function from some index set to the subbases of each factor space. (Contributed by Mario Carneiro, 3-Feb-2015.)
Assertion
Ref Expression
df-pt  |-  Xt_  =  ( f  e.  _V  |->  ( topGen `  { x  |  E. g ( ( g  Fn  dom  f  /\  A. y  e.  dom  f ( g `  y )  e.  ( f `  y )  /\  E. z  e. 
Fin  A. y  e.  ( dom  f  \  z
) ( g `  y )  =  U. ( f `  y
) )  /\  x  =  X_ y  e.  dom  f ( g `  y ) ) } ) )
Distinct variable group:    f, g, x, y, z

Detailed syntax breakdown of Definition df-pt
StepHypRef Expression
1 cpt 13343 . 2  class  Xt_
2 vf . . 3  set  f
3 cvv 2788 . . 3  class  _V
4 vg . . . . . . . . . 10  set  g
54cv 1622 . . . . . . . . 9  class  g
62cv 1622 . . . . . . . . . 10  class  f
76cdm 4689 . . . . . . . . 9  class  dom  f
85, 7wfn 5250 . . . . . . . 8  wff  g  Fn 
dom  f
9 vy . . . . . . . . . . . 12  set  y
109cv 1622 . . . . . . . . . . 11  class  y
1110, 5cfv 5255 . . . . . . . . . 10  class  ( g `
 y )
1210, 6cfv 5255 . . . . . . . . . 10  class  ( f `
 y )
1311, 12wcel 1684 . . . . . . . . 9  wff  ( g `
 y )  e.  ( f `  y
)
1413, 9, 7wral 2543 . . . . . . . 8  wff  A. y  e.  dom  f ( g `
 y )  e.  ( f `  y
)
1512cuni 3827 . . . . . . . . . . 11  class  U. (
f `  y )
1611, 15wceq 1623 . . . . . . . . . 10  wff  ( g `
 y )  = 
U. ( f `  y )
17 vz . . . . . . . . . . . 12  set  z
1817cv 1622 . . . . . . . . . . 11  class  z
197, 18cdif 3149 . . . . . . . . . 10  class  ( dom  f  \  z )
2016, 9, 19wral 2543 . . . . . . . . 9  wff  A. y  e.  ( dom  f  \ 
z ) ( g `
 y )  = 
U. ( f `  y )
21 cfn 6863 . . . . . . . . 9  class  Fin
2220, 17, 21wrex 2544 . . . . . . . 8  wff  E. z  e.  Fin  A. y  e.  ( dom  f  \ 
z ) ( g `
 y )  = 
U. ( f `  y )
238, 14, 22w3a 934 . . . . . . 7  wff  ( g  Fn  dom  f  /\  A. y  e.  dom  f
( g `  y
)  e.  ( f `
 y )  /\  E. z  e.  Fin  A. y  e.  ( dom  f  \  z ) ( g `  y )  =  U. ( f `
 y ) )
24 vx . . . . . . . . 9  set  x
2524cv 1622 . . . . . . . 8  class  x
269, 7, 11cixp 6817 . . . . . . . 8  class  X_ y  e.  dom  f ( g `
 y )
2725, 26wceq 1623 . . . . . . 7  wff  x  = 
X_ y  e.  dom  f ( g `  y )
2823, 27wa 358 . . . . . 6  wff  ( ( g  Fn  dom  f  /\  A. y  e.  dom  f ( g `  y )  e.  ( f `  y )  /\  E. z  e. 
Fin  A. y  e.  ( dom  f  \  z
) ( g `  y )  =  U. ( f `  y
) )  /\  x  =  X_ y  e.  dom  f ( g `  y ) )
2928, 4wex 1528 . . . . 5  wff  E. g
( ( g  Fn 
dom  f  /\  A. y  e.  dom  f ( g `  y )  e.  ( f `  y )  /\  E. z  e.  Fin  A. y  e.  ( dom  f  \ 
z ) ( g `
 y )  = 
U. ( f `  y ) )  /\  x  =  X_ y  e. 
dom  f ( g `
 y ) )
3029, 24cab 2269 . . . 4  class  { x  |  E. g ( ( g  Fn  dom  f  /\  A. y  e.  dom  f ( g `  y )  e.  ( f `  y )  /\  E. z  e. 
Fin  A. y  e.  ( dom  f  \  z
) ( g `  y )  =  U. ( f `  y
) )  /\  x  =  X_ y  e.  dom  f ( g `  y ) ) }
31 ctg 13342 . . . 4  class  topGen
3230, 31cfv 5255 . . 3  class  ( topGen `  { x  |  E. g ( ( g  Fn  dom  f  /\  A. y  e.  dom  f
( g `  y
)  e.  ( f `
 y )  /\  E. z  e.  Fin  A. y  e.  ( dom  f  \  z ) ( g `  y )  =  U. ( f `
 y ) )  /\  x  =  X_ y  e.  dom  f ( g `  y ) ) } )
332, 3, 32cmpt 4077 . 2  class  ( f  e.  _V  |->  ( topGen `  { x  |  E. g ( ( g  Fn  dom  f  /\  A. y  e.  dom  f
( g `  y
)  e.  ( f `
 y )  /\  E. z  e.  Fin  A. y  e.  ( dom  f  \  z ) ( g `  y )  =  U. ( f `
 y ) )  /\  x  =  X_ y  e.  dom  f ( g `  y ) ) } ) )
341, 33wceq 1623 1  wff  Xt_  =  ( f  e.  _V  |->  ( topGen `  { x  |  E. g ( ( g  Fn  dom  f  /\  A. y  e.  dom  f ( g `  y )  e.  ( f `  y )  /\  E. z  e. 
Fin  A. y  e.  ( dom  f  \  z
) ( g `  y )  =  U. ( f `  y
) )  /\  x  =  X_ y  e.  dom  f ( g `  y ) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  ptval  17265
  Copyright terms: Public domain W3C validator