Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prtop Unicode version

Definition df-prtop 25545
Description: The product topology of a family  f of topologies is the coarsest topology over the product of the underlying sets that makes the projections continuous. (Bourbaki TG I.14 ex. 3) Experimental. (Contributed by FL, 4-Dec-2011.)
Assertion
Ref Expression
df-prtop  |-  topX  =  { <. f ,  y
>.  |  ( f : dom  f --> Top  /\  y  =  |^| { t  e.  Top  |  ( U. t  =  X_ x  e.  dom  f U. ( f `  x
)  /\  A. i  e.  dom  f ( X_ x  e.  dom  f U. ( f `  x
)  pr  i )  e.  ( t  Cn  ( f `  i
) ) ) } ) }
Distinct variable group:    y, f, t, x, i

Detailed syntax breakdown of Definition df-prtop
StepHypRef Expression
1 ctopx 25544 . 2  class  topX
2 vf . . . . . . 7  set  f
32cv 1622 . . . . . 6  class  f
43cdm 4689 . . . . 5  class  dom  f
5 ctop 16631 . . . . 5  class  Top
64, 5, 3wf 5251 . . . 4  wff  f : dom  f --> Top
7 vy . . . . . 6  set  y
87cv 1622 . . . . 5  class  y
9 vt . . . . . . . . . . 11  set  t
109cv 1622 . . . . . . . . . 10  class  t
1110cuni 3827 . . . . . . . . 9  class  U. t
12 vx . . . . . . . . . 10  set  x
1312cv 1622 . . . . . . . . . . . 12  class  x
1413, 3cfv 5255 . . . . . . . . . . 11  class  ( f `
 x )
1514cuni 3827 . . . . . . . . . 10  class  U. (
f `  x )
1612, 4, 15cixp 6817 . . . . . . . . 9  class  X_ x  e.  dom  f U. (
f `  x )
1711, 16wceq 1623 . . . . . . . 8  wff  U. t  =  X_ x  e.  dom  f U. ( f `  x )
18 vi . . . . . . . . . . . 12  set  i
1918cv 1622 . . . . . . . . . . 11  class  i
20 cpro 25150 . . . . . . . . . . 11  class  pr
2116, 19, 20co 5858 . . . . . . . . . 10  class  ( X_ x  e.  dom  f U. ( f `  x
)  pr  i )
2219, 3cfv 5255 . . . . . . . . . . 11  class  ( f `
 i )
23 ccn 16954 . . . . . . . . . . 11  class  Cn
2410, 22, 23co 5858 . . . . . . . . . 10  class  ( t  Cn  ( f `  i ) )
2521, 24wcel 1684 . . . . . . . . 9  wff  ( X_ x  e.  dom  f U. ( f `  x
)  pr  i )  e.  ( t  Cn  ( f `  i
) )
2625, 18, 4wral 2543 . . . . . . . 8  wff  A. i  e.  dom  f ( X_ x  e.  dom  f U. ( f `  x
)  pr  i )  e.  ( t  Cn  ( f `  i
) )
2717, 26wa 358 . . . . . . 7  wff  ( U. t  =  X_ x  e. 
dom  f U. (
f `  x )  /\  A. i  e.  dom  f ( X_ x  e.  dom  f U. (
f `  x )  pr  i )  e.  ( t  Cn  ( f `
 i ) ) )
2827, 9, 5crab 2547 . . . . . 6  class  { t  e.  Top  |  ( U. t  =  X_ x  e.  dom  f U. ( f `  x
)  /\  A. i  e.  dom  f ( X_ x  e.  dom  f U. ( f `  x
)  pr  i )  e.  ( t  Cn  ( f `  i
) ) ) }
2928cint 3862 . . . . 5  class  |^| { t  e.  Top  |  ( U. t  =  X_ x  e.  dom  f U. ( f `  x
)  /\  A. i  e.  dom  f ( X_ x  e.  dom  f U. ( f `  x
)  pr  i )  e.  ( t  Cn  ( f `  i
) ) ) }
308, 29wceq 1623 . . . 4  wff  y  = 
|^| { t  e.  Top  |  ( U. t  = 
X_ x  e.  dom  f U. ( f `  x )  /\  A. i  e.  dom  f (
X_ x  e.  dom  f U. ( f `  x )  pr  i
)  e.  ( t  Cn  ( f `  i ) ) ) }
316, 30wa 358 . . 3  wff  ( f : dom  f --> Top 
/\  y  =  |^| { t  e.  Top  | 
( U. t  = 
X_ x  e.  dom  f U. ( f `  x )  /\  A. i  e.  dom  f (
X_ x  e.  dom  f U. ( f `  x )  pr  i
)  e.  ( t  Cn  ( f `  i ) ) ) } )
3231, 2, 7copab 4076 . 2  class  { <. f ,  y >.  |  ( f : dom  f --> Top  /\  y  =  |^| { t  e.  Top  | 
( U. t  = 
X_ x  e.  dom  f U. ( f `  x )  /\  A. i  e.  dom  f (
X_ x  e.  dom  f U. ( f `  x )  pr  i
)  e.  ( t  Cn  ( f `  i ) ) ) } ) }
331, 32wceq 1623 1  wff  topX  =  { <. f ,  y
>.  |  ( f : dom  f --> Top  /\  y  =  |^| { t  e.  Top  |  ( U. t  =  X_ x  e.  dom  f U. ( f `  x
)  /\  A. i  e.  dom  f ( X_ x  e.  dom  f U. ( f `  x
)  pr  i )  e.  ( t  Cn  ( f `  i
) ) ) } ) }
Colors of variables: wff set class
This definition is referenced by:  istopx  25547
  Copyright terms: Public domain W3C validator