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

Theorem ptval 21653
Description: The value of the product topology function. (Contributed by Mario Carneiro, 3-Feb-2015.)
Hypothesis
Ref Expression
ptval.1 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}
Assertion
Ref Expression
ptval ((𝐴𝑉𝐹 Fn 𝐴) → (∏t𝐹) = (topGen‘𝐵))
Distinct variable groups:   𝑥,𝑔,𝑦,𝑧,𝐴   𝑔,𝐹,𝑥,𝑦,𝑧   𝑔,𝑉,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑧,𝑔)

Proof of Theorem ptval
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 df-pt 16373 . . 3 t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}))
21a1i 11 . 2 ((𝐴𝑉𝐹 Fn 𝐴) → ∏t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))})))
3 simpr 477 . . . . . . . . . . 11 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹)
43dmeqd 5494 . . . . . . . . . 10 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → dom 𝑓 = dom 𝐹)
5 fndm 6168 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
65ad2antlr 718 . . . . . . . . . 10 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → dom 𝐹 = 𝐴)
74, 6eqtrd 2799 . . . . . . . . 9 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → dom 𝑓 = 𝐴)
87fneq2d 6160 . . . . . . . 8 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (𝑔 Fn dom 𝑓𝑔 Fn 𝐴))
93fveq1d 6377 . . . . . . . . . 10 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (𝑓𝑦) = (𝐹𝑦))
109eleq2d 2830 . . . . . . . . 9 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → ((𝑔𝑦) ∈ (𝑓𝑦) ↔ (𝑔𝑦) ∈ (𝐹𝑦)))
117, 10raleqbidv 3300 . . . . . . . 8 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ↔ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦)))
127difeq1d 3889 . . . . . . . . . 10 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (dom 𝑓𝑧) = (𝐴𝑧))
139unieqd 4604 . . . . . . . . . . 11 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (𝑓𝑦) = (𝐹𝑦))
1413eqeq2d 2775 . . . . . . . . . 10 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → ((𝑔𝑦) = (𝑓𝑦) ↔ (𝑔𝑦) = (𝐹𝑦)))
1512, 14raleqbidv 3300 . . . . . . . . 9 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦) ↔ ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)))
1615rexbidv 3199 . . . . . . . 8 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦) ↔ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)))
178, 11, 163anbi123d 1560 . . . . . . 7 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → ((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ↔ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦))))
187ixpeq1d 8125 . . . . . . . 8 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → X𝑦 ∈ dom 𝑓(𝑔𝑦) = X𝑦𝐴 (𝑔𝑦))
1918eqeq2d 2775 . . . . . . 7 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦) ↔ 𝑥 = X𝑦𝐴 (𝑔𝑦)))
2017, 19anbi12d 624 . . . . . 6 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦)) ↔ ((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))))
2120exbidv 2016 . . . . 5 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦)) ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))))
2221abbidv 2884 . . . 4 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → {𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))})
23 ptval.1 . . . 4 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}
2422, 23syl6eqr 2817 . . 3 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → {𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))} = 𝐵)
2524fveq2d 6379 . 2 (((𝐴𝑉𝐹 Fn 𝐴) ∧ 𝑓 = 𝐹) → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔𝑦) ∈ (𝑓𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓𝑧)(𝑔𝑦) = (𝑓𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔𝑦))}) = (topGen‘𝐵))
26 fnex 6674 . . 3 ((𝐹 Fn 𝐴𝐴𝑉) → 𝐹 ∈ V)
2726ancoms 450 . 2 ((𝐴𝑉𝐹 Fn 𝐴) → 𝐹 ∈ V)
28 fvexd 6390 . 2 ((𝐴𝑉𝐹 Fn 𝐴) → (topGen‘𝐵) ∈ V)
292, 25, 27, 28fvmptd 6477 1 ((𝐴𝑉𝐹 Fn 𝐴) → (∏t𝐹) = (topGen‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  {cab 2751  wral 3055  wrex 3056  Vcvv 3350  cdif 3729   cuni 4594  cmpt 4888  dom cdm 5277   Fn wfn 6063  cfv 6068  Xcixp 8113  Fincfn 8160  topGenctg 16366  tcpt 16367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ixp 8114  df-pt 16373
This theorem is referenced by:  pttop  21665  ptopn  21666  ptuni  21677  ptval2  21684  ptpjcn  21694  ptpjopn  21695  ptclsg  21698  ptcnp  21705  prdstopn  21711  xkoptsub  21737  ptcmplem1  22135  tmdgsum2  22179  prdsxmslem2  22613  ptrecube  33765
  Copyright terms: Public domain W3C validator