Definition df-pt 12932

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 12926	. 2 class ∏t
2		vf	. . 3 setvar 𝑓
3		cvv 2763	. . 3 class V
4		vg	. . . . . . . . . 10 setvar 𝑔
5	4	cv 1363	. . . . . . . . 9 class 𝑔
6	2	cv 1363	. . . . . . . . . 10 class 𝑓
7	6	cdm 4663	. . . . . . . . 9 class dom 𝑓
8	5, 7	wfn 5253	. . . . . . . 8 wff 𝑔 Fn dom 𝑓
9		vy	. . . . . . . . . . . 12 setvar 𝑦
10	9	cv 1363	. . . . . . . . . . 11 class 𝑦
11	10, 5	cfv 5258	. . . . . . . . . 10 class (𝑔‘𝑦)
12	10, 6	cfv 5258	. . . . . . . . . 10 class (𝑓‘𝑦)
13	11, 12	wcel 2167	. . . . . . . . 9 wff (𝑔‘𝑦) ∈ (𝑓‘𝑦)
14	13, 9, 7	wral 2475	. . . . . . . 8 wff ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦)
15	12	cuni 3839	. . . . . . . . . . 11 class ∪ (𝑓‘𝑦)
16	11, 15	wceq 1364	. . . . . . . . . 10 wff (𝑔‘𝑦) = ∪ (𝑓‘𝑦)
17		vz	. . . . . . . . . . . 12 setvar 𝑧
18	17	cv 1363	. . . . . . . . . . 11 class 𝑧
19	7, 18	cdif 3154	. . . . . . . . . 10 class (dom 𝑓 ∖ 𝑧)
20	16, 9, 19	wral 2475	. . . . . . . . 9 wff ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)
21		cfn 6799	. . . . . . . . 9 class Fin
22	20, 17, 21	wrex 2476	. . . . . . . 8 wff ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)
23	8, 14, 22	w3a 980	. . . . . . 7 wff (𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦))
24		vx	. . . . . . . . 9 setvar 𝑥
25	24	cv 1363	. . . . . . . 8 class 𝑥
26	9, 7, 11	cixp 6757	. . . . . . . 8 class X𝑦 ∈ dom 𝑓(𝑔‘𝑦)
27	25, 26	wceq 1364	. . . . . . 7 wff 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦)
28	23, 27	wa 104	. . . . . 6 wff ((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))
29	28, 4	wex 1506	. . . . 5 wff ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))
30	29, 24	cab 2182	. . . 4 class {𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}
31		ctg 12925	. . . 4 class topGen
32	30, 31	cfv 5258	. . 3 class (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))})
33	2, 3, 32	cmpt 4094	. 2 class (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}))
34	1, 33	wceq 1364	1 wff ∏t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}))

This definition is referenced by:  ptex  12935