ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-pt GIF version

Definition df-pt 12443
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
StepHypRef Expression
1 cpt 12437 . 2 class t
2 vf . . 3 setvar 𝑓
3 cvv 2712 . . 3 class V
4 vg . . . . . . . . . 10 setvar 𝑔
54cv 1334 . . . . . . . . 9 class 𝑔
62cv 1334 . . . . . . . . . 10 class 𝑓
76cdm 4588 . . . . . . . . 9 class dom 𝑓
85, 7wfn 5167 . . . . . . . 8 wff 𝑔 Fn dom 𝑓
9 vy . . . . . . . . . . . 12 setvar 𝑦
109cv 1334 . . . . . . . . . . 11 class 𝑦
1110, 5cfv 5172 . . . . . . . . . 10 class (𝑔𝑦)
1210, 6cfv 5172 . . . . . . . . . 10 class (𝑓𝑦)
1311, 12wcel 2128 . . . . . . . . 9 wff (𝑔𝑦) ∈ (𝑓𝑦)
1413, 9, 7wral 2435 . . . . . . . 8 wff 𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦)
1512cuni 3774 . . . . . . . . . . 11 class (𝑓𝑦)
1611, 15wceq 1335 . . . . . . . . . 10 wff (𝑔𝑦) = (𝑓𝑦)
17 vz . . . . . . . . . . . 12 setvar 𝑧
1817cv 1334 . . . . . . . . . . 11 class 𝑧
197, 18cdif 3099 . . . . . . . . . 10 class (dom 𝑓𝑧)
2016, 9, 19wral 2435 . . . . . . . . 9 wff 𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)
21 cfn 6687 . . . . . . . . 9 class Fin
2220, 17, 21wrex 2436 . . . . . . . 8 wff 𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)
238, 14, 22w3a 963 . . . . . . 7 wff (𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦))
24 vx . . . . . . . . 9 setvar 𝑥
2524cv 1334 . . . . . . . 8 class 𝑥
269, 7, 11cixp 6645 . . . . . . . 8 class X𝑦 ∈ dom 𝑓(𝑔𝑦)
2725, 26wceq 1335 . . . . . . 7 wff 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦)
2823, 27wa 103 . . . . . 6 wff ((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))
2928, 4wex 1472 . . . . 5 wff 𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))
3029, 24cab 2143 . . . 4 class {𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}
31 ctg 12436 . . . 4 class topGen
3230, 31cfv 5172 . . 3 class (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))})
332, 3, 32cmpt 4027 . 2 class (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}))
341, 33wceq 1335 1 wff t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}))
Colors of variables: wff set class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator