Metamath Proof Explorer

Definition df-pt

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)

Ref Expression
Assertion 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 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpt 
 |-  Xt_
1 vf 
 |-  f
2 cvv 
 |-  _V
3 ctg 
 |-  topGen
4 vx 
 |-  x
5 vg 
 |-  g
6 5 cv 
 |-  g
7 1 cv 
 |-  f
8 7 cdm 
 |-  dom f
9 6 8 wfn 
 |-  g Fn dom f
10 vy 
 |-  y
11 10 cv 
 |-  y
12 11 6 cfv 
 |-  ( g ` y )
13 11 7 cfv 
 |-  ( f ` y )
14 12 13 wcel 
 |-  ( g ` y ) e. ( f ` y )
15 14 10 8 wral 
 |-  A. y e. dom f ( g ` y ) e. ( f ` y )
16 vz 
 |-  z
17 cfn 
 |-  Fin
18 16 cv 
 |-  z
19 8 18 cdif 
 |-  ( dom f \ z )
20 13 cuni 
 |-  U. ( f ` y )
21 12 20 wceq 
 |-  ( g ` y ) = U. ( f ` y )
22 21 10 19 wral 
 |-  A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y )
23 22 16 17 wrex 
 |-  E. z e. Fin A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y )
24 9 15 23 w3a 
 |-  ( 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 ) )
25 4 cv 
 |-  x
26 10 8 12 cixp 
 |-  X_ y e. dom f ( g ` y )
27 25 26 wceq 
 |-  x = X_ y e. dom f ( g ` y )
28 24 27 wa 
 |-  ( ( 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 ) )
29 28 5 wex 
 |-  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 ) )
30 29 4 cab 
 |-  { 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 30 3 cfv 
 |-  ( 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 ) ) } )
32 1 2 31 cmpt 
 |-  ( 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 ) ) } ) )
33 0 32 wceq 
 |-  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 ) ) } ) )