MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pt Structured version   Visualization version   GIF version

Definition df-pt 15928
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 15922 . 2 class t
2 vf . . 3 setvar 𝑓
3 cvv 3173 . . 3 class V
4 vg . . . . . . . . . 10 setvar 𝑔
54cv 1474 . . . . . . . . 9 class 𝑔
62cv 1474 . . . . . . . . . 10 class 𝑓
76cdm 5038 . . . . . . . . 9 class dom 𝑓
85, 7wfn 5799 . . . . . . . 8 wff 𝑔 Fn dom 𝑓
9 vy . . . . . . . . . . . 12 setvar 𝑦
109cv 1474 . . . . . . . . . . 11 class 𝑦
1110, 5cfv 5804 . . . . . . . . . 10 class (𝑔𝑦)
1210, 6cfv 5804 . . . . . . . . . 10 class (𝑓𝑦)
1311, 12wcel 1977 . . . . . . . . 9 wff (𝑔𝑦) ∈ (𝑓𝑦)
1413, 9, 7wral 2896 . . . . . . . 8 wff 𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦)
1512cuni 4372 . . . . . . . . . . 11 class (𝑓𝑦)
1611, 15wceq 1475 . . . . . . . . . 10 wff (𝑔𝑦) = (𝑓𝑦)
17 vz . . . . . . . . . . . 12 setvar 𝑧
1817cv 1474 . . . . . . . . . . 11 class 𝑧
197, 18cdif 3537 . . . . . . . . . 10 class (dom 𝑓𝑧)
2016, 9, 19wral 2896 . . . . . . . . 9 wff 𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)
21 cfn 7841 . . . . . . . . 9 class Fin
2220, 17, 21wrex 2897 . . . . . . . 8 wff 𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)
238, 14, 22w3a 1031 . . . . . . 7 wff (𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦))
24 vx . . . . . . . . 9 setvar 𝑥
2524cv 1474 . . . . . . . 8 class 𝑥
269, 7, 11cixp 7794 . . . . . . . 8 class X𝑦 ∈ dom 𝑓(𝑔𝑦)
2725, 26wceq 1475 . . . . . . 7 wff 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦)
2823, 27wa 383 . . . . . 6 wff ((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))
2928, 4wex 1695 . . . . 5 wff 𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))
3029, 24cab 2596 . . . 4 class {𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}
31 ctg 15921 . . . 4 class topGen
3230, 31cfv 5804 . . 3 class (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))})
332, 3, 32cmpt 4643 . 2 class (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}))
341, 33wceq 1475 1 wff t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}))
Colors of variables: wff setvar class
This definition is referenced by:  ptval  21183
  Copyright terms: Public domain W3C validator