Definition df-pt 12710

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

Step	Hyp	Ref	Expression
1		cpt 12704	. 2 class Xt_
2		vf	. . 3 setvar f
3		cvv 2738	. . 3 class _V
4		vg	. . . . . . . . . 10 setvar g
5	4	cv 1352	. . . . . . . . 9 class g
6	2	cv 1352	. . . . . . . . . 10 class f
7	6	cdm 4627	. . . . . . . . 9 class dom f
8	5, 7	wfn 5212	. . . . . . . 8 wff g Fn dom f
9		vy	. . . . . . . . . . . 12 setvar y
10	9	cv 1352	. . . . . . . . . . 11 class y
11	10, 5	cfv 5217	. . . . . . . . . 10 class ( g ` y )
12	10, 6	cfv 5217	. . . . . . . . . 10 class ( f ` y )
13	11, 12	wcel 2148	. . . . . . . . 9 wff ( g ` y ) e. ( f ` y )
14	13, 9, 7	wral 2455	. . . . . . . 8 wff A. y e. dom f ( g ` y ) e. ( f ` y )
15	12	cuni 3810	. . . . . . . . . . 11 class U. ( f ` y )
16	11, 15	wceq 1353	. . . . . . . . . 10 wff ( g ` y ) = U. ( f ` y )
17		vz	. . . . . . . . . . . 12 setvar z
18	17	cv 1352	. . . . . . . . . . 11 class z
19	7, 18	cdif 3127	. . . . . . . . . 10 class ( dom f \ z )
20	16, 9, 19	wral 2455	. . . . . . . . 9 wff A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y )
21		cfn 6740	. . . . . . . . 9 class Fin
22	20, 17, 21	wrex 2456	. . . . . . . 8 wff E. z e. Fin A. y e. ( dom f \ z ) ( g ` y ) = U. ( f ` y )
23	8, 14, 22	w3a 978	. . . . . . 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 setvar x
25	24	cv 1352	. . . . . . . 8 class x
26	9, 7, 11	cixp 6698	. . . . . . . 8 class X_ y e. dom f ( g ` y )
27	25, 26	wceq 1353	. . . . . . 7 wff x = X_ y e. dom f ( g ` y )
28	23, 27	wa 104	. . . . . 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 ) )
29	28, 4	wex 1492	. . . . 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 ) )
30	29, 24	cab 2163	. . . 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 12703	. . . 4 class topGen
32	30, 31	cfv 5217	. . 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 ) ) } )
33	2, 3, 32	cmpt 4065	. 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 ) ) } ) )
34	1, 33	wceq 1353	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 ) ) } ) )

This definition is referenced by:  ptex  12713