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	$⊢ \prod_{𝑡} = (f \in V ⟼ topGen (\{x \| \exists g ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} g (y))\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpt	$class \prod_{𝑡}$
1		vf	$setvar f$
2		cvv	$class V$
3		ctg	$class topGen$
4		vx	$setvar x$
5		vg	$setvar g$
6	5	cv	$setvar g$
7	1	cv	$setvar f$
8	7	cdm	$class dom f$
9	6 8	wfn	$wff g Fn dom f$
10		vy	$setvar y$
11	10	cv	$setvar y$
12	11 6	cfv	$class g (y)$
13	11 7	cfv	$class f (y)$
14	12 13	wcel	$wff g (y) \in f (y)$
15	14 10 8	wral	$wff \forall y \in dom f g (y) \in f (y)$
16		vz	$setvar z$
17		cfn	$class Fin$
18	16	cv	$setvar z$
19	8 18	cdif	$class (dom f ∖ z)$
20	13	cuni	$class ⋃ f (y)$
21	12 20	wceq	$wff g (y) = ⋃ f (y)$
22	21 10 19	wral	$wff \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)$
23	22 16 17	wrex	$wff \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)$
24	9 15 23	w3a	$wff (g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y))$
25	4	cv	$setvar x$
26	10 8 12	cixp	$class \underset{y \in dom f}{⨉} g (y)$
27	25 26	wceq	$wff x = \underset{y \in dom f}{⨉} g (y)$
28	24 27	wa	$wff ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} g (y))$
29	28 5	wex	$wff \exists g ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} g (y))$
30	29 4	cab	$class \{x \| \exists g ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} g (y))\}$
31	30 3	cfv	$class topGen (\{x \| \exists g ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} g (y))\})$
32	1 2 31	cmpt	$class (f \in V ⟼ topGen (\{x \| \exists g ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} g (y))\}))$
33	0 32	wceq	$wff \prod_{𝑡} = (f \in V ⟼ topGen (\{x \| \exists g ((g Fn dom f \land \forall y \in dom f g (y) \in f (y) \land \exists z \in Fin \forall y \in (dom f ∖ z) g (y) = ⋃ f (y)) \land x = \underset{y \in dom f}{⨉} g (y))\}))$

Metamath Proof Explorer

Definition df-pt

Detailed syntax breakdown