Definition df-pt 13598

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	⊢ ∏t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}))

Distinct variable group:   𝑓,𝑔,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-pt

Step	Hyp	Ref	Expression
1		cpt 13592	. 2 class ∏t
2		vf	. . 3 setvar 𝑓
3		cvv 2821	. . 3 class V
4		vg	. . . . . . . . . 10 setvar 𝑔
5	4	cv 1401	. . . . . . . . 9 class 𝑔
6	2	cv 1401	. . . . . . . . . 10 class 𝑓
7	6	cdm 4772	. . . . . . . . 9 class dom 𝑓
8	5, 7	wfn 5370	. . . . . . . 8 wff 𝑔 Fn dom 𝑓
9		vy	. . . . . . . . . . . 12 setvar 𝑦
10	9	cv 1401	. . . . . . . . . . 11 class 𝑦
11	10, 5	cfv 5375	. . . . . . . . . 10 class (𝑔‘𝑦)
12	10, 6	cfv 5375	. . . . . . . . . 10 class (𝑓‘𝑦)
13	11, 12	wcel 2209	. . . . . . . . 9 wff (𝑔‘𝑦) ∈ (𝑓‘𝑦)
14	13, 9, 7	wral 2528	. . . . . . . 8 wff ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦)
15	12	cuni 3933	. . . . . . . . . . 11 class ∪ (𝑓‘𝑦)
16	11, 15	wceq 1402	. . . . . . . . . 10 wff (𝑔‘𝑦) = ∪ (𝑓‘𝑦)
17		vz	. . . . . . . . . . . 12 setvar 𝑧
18	17	cv 1401	. . . . . . . . . . 11 class 𝑧
19	7, 18	cdif 3217	. . . . . . . . . 10 class (dom 𝑓 ∖ 𝑧)
20	16, 9, 19	wral 2528	. . . . . . . . 9 wff ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)
21		cfn 7016	. . . . . . . . 9 class Fin
22	20, 17, 21	wrex 2529	. . . . . . . 8 wff ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)
23	8, 14, 22	w3a 1009	. . . . . . 7 wff (𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦))
24		vx	. . . . . . . . 9 setvar 𝑥
25	24	cv 1401	. . . . . . . 8 class 𝑥
26	9, 7, 11	cixp 6974	. . . . . . . 8 class X𝑦 ∈ dom 𝑓(𝑔‘𝑦)
27	25, 26	wceq 1402	. . . . . . 7 wff 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦)
28	23, 27	wa 104	. . . . . 6 wff ((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))
29	28, 4	wex 1545	. . . . 5 wff ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))
30	29, 24	cab 2224	. . . 4 class {𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}
31		ctg 13591	. . . 4 class topGen
32	30, 31	cfv 5375	. . 3 class (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))})
33	2, 3, 32	cmpt 4190	. 2 class (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}))
34	1, 33	wceq 1402	1 wff ∏t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}))

This definition is referenced by:  ptex  13601