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 16708
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 16702 . 2 class t
2 vf . . 3 setvar 𝑓
3 cvv 3495 . . 3 class V
4 vg . . . . . . . . . 10 setvar 𝑔
54cv 1527 . . . . . . . . 9 class 𝑔
62cv 1527 . . . . . . . . . 10 class 𝑓
76cdm 5549 . . . . . . . . 9 class dom 𝑓
85, 7wfn 6344 . . . . . . . 8 wff 𝑔 Fn dom 𝑓
9 vy . . . . . . . . . . . 12 setvar 𝑦
109cv 1527 . . . . . . . . . . 11 class 𝑦
1110, 5cfv 6349 . . . . . . . . . 10 class (𝑔𝑦)
1210, 6cfv 6349 . . . . . . . . . 10 class (𝑓𝑦)
1311, 12wcel 2105 . . . . . . . . 9 wff (𝑔𝑦) ∈ (𝑓𝑦)
1413, 9, 7wral 3138 . . . . . . . 8 wff 𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦)
1512cuni 4832 . . . . . . . . . . 11 class (𝑓𝑦)
1611, 15wceq 1528 . . . . . . . . . 10 wff (𝑔𝑦) = (𝑓𝑦)
17 vz . . . . . . . . . . . 12 setvar 𝑧
1817cv 1527 . . . . . . . . . . 11 class 𝑧
197, 18cdif 3932 . . . . . . . . . 10 class (dom 𝑓𝑧)
2016, 9, 19wral 3138 . . . . . . . . 9 wff 𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)
21 cfn 8498 . . . . . . . . 9 class Fin
2220, 17, 21wrex 3139 . . . . . . . 8 wff 𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)
238, 14, 22w3a 1079 . . . . . . 7 wff (𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦))
24 vx . . . . . . . . 9 setvar 𝑥
2524cv 1527 . . . . . . . 8 class 𝑥
269, 7, 11cixp 8450 . . . . . . . 8 class X𝑦 ∈ dom 𝑓(𝑔𝑦)
2725, 26wceq 1528 . . . . . . 7 wff 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦)
2823, 27wa 396 . . . . . 6 wff ((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))
2928, 4wex 1771 . . . . 5 wff 𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))
3029, 24cab 2799 . . . 4 class {𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}
31 ctg 16701 . . . 4 class topGen
3230, 31cfv 6349 . . 3 class (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))})
332, 3, 32cmpt 5138 . 2 class (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}))
341, 33wceq 1528 1 wff t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}))
Colors of variables: wff setvar class
This definition is referenced by:  ptval  22108
  Copyright terms: Public domain W3C validator