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

Definition df-pt 13340
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 13338 . 2  class  Xt_
2 vf . . 3  set  f
3 cvv 2790 . . 3  class  _V
4 vg . . . . . . . . . 10  set  g
54cv 1623 . . . . . . . . 9  class  g
62cv 1623 . . . . . . . . . 10  class  f
76cdm 4689 . . . . . . . . 9  class  dom  f
85, 7wfn 5217 . . . . . . . 8  wff  g  Fn 
dom  f
9 vy . . . . . . . . . . . 12  set  y
109cv 1623 . . . . . . . . . . 11  class  y
1110, 5cfv 5222 . . . . . . . . . 10  class  ( g `
 y )
1210, 6cfv 5222 . . . . . . . . . 10  class  ( f `
 y )
1311, 12wcel 1685 . . . . . . . . 9  wff  ( g `
 y )  e.  ( f `  y
)
1413, 9, 7wral 2545 . . . . . . . 8  wff  A. y  e.  dom  f ( g `
 y )  e.  ( f `  y
)
1512cuni 3829 . . . . . . . . . . 11  class  U. (
f `  y )
1611, 15wceq 1624 . . . . . . . . . 10  wff  ( g `
 y )  = 
U. ( f `  y )
17 vz . . . . . . . . . . . 12  set  z
1817cv 1623 . . . . . . . . . . 11  class  z
197, 18cdif 3151 . . . . . . . . . 10  class  ( dom  f  \  z )
2016, 9, 19wral 2545 . . . . . . . . 9  wff  A. y  e.  ( dom  f  \ 
z ) ( g `
 y )  = 
U. ( f `  y )
21 cfn 6859 . . . . . . . . 9  class  Fin
2220, 17, 21wrex 2546 . . . . . . . 8  wff  E. z  e.  Fin  A. y  e.  ( dom  f  \ 
z ) ( g `
 y )  = 
U. ( f `  y )
238, 14, 22w3a 936 . . . . . . 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 1623 . . . . . . . 8  class  x
269, 7, 11cixp 6813 . . . . . . . 8  class  X_ y  e.  dom  f ( g `
 y )
2725, 26wceq 1624 . . . . . . 7  wff  x  = 
X_ y  e.  dom  f ( g `  y )
2823, 27wa 360 . . . . . 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 1529 . . . . 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 2271 . . . 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 13337 . . . 4  class  topGen
3230, 31cfv 5222 . . 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 4079 . 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 1624 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  17260
  Copyright terms: Public domain W3C validator