Theorem reldmpsr 21904

Description: The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)

Assertion

Ref	Expression
reldmpsr	⊢ Rel dom mPwSer

Proof of Theorem reldmpsr

Dummy variables ℎ 𝑖 𝑟 𝑦 𝑏 𝑑 𝑓 𝑔 𝑘 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-psr 21899	. 2 ⊢ mPwSer = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋{ℎ ∈ (ℕ0 ↑m 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} / 𝑑⦌⦋((Base‘𝑟) ↑m 𝑑) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), ( ∘f (+g‘𝑟) ↾ (𝑏 × 𝑏))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑘 ∈ 𝑑 ↦ (𝑟 Σg (𝑥 ∈ {𝑦 ∈ 𝑑 ∣ 𝑦 ∘r ≤ 𝑘} ↦ ((𝑓‘𝑥)(.r‘𝑟)(𝑔‘(𝑘 ∘f − 𝑥)))))))⟩} ∪ {⟨(Scalar‘ndx), 𝑟⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘𝑟), 𝑓 ∈ 𝑏 ↦ ((𝑑 × {𝑥}) ∘f (.r‘𝑟)𝑓))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑑 × {(TopOpen‘𝑟)}))⟩}))
2	1	reldmmpo 7494	1 ⊢ Rel dom mPwSer

Syntax hints:   ∈ wcel 2114  {crab 3390  Vcvv 3430  ⦋csb 3838   ∪ cun 3888  {csn 4568  {ctp 4572  ⟨cop 4574   class class class wbr 5086   ↦ cmpt 5167   × cxp 5622  ^◡ccnv 5623  dom cdm 5624   ↾ cres 5626   “ cima 5627  Rel wrel 5629  ‘cfv 6492  (class class class)co 7360   ∈ cmpo 7362   ∘_f cof 7622   ∘_r cofr 7623   ↑_m cmap 8766  Fincfn 8886   ≤ cle 11171   − cmin 11368  ℕcn 12165  ℕ₀cn0 12428  ndxcnx 17154  Basecbs 17170  +_gcplusg 17211  ._rcmulr 17212  Scalarcsca 17214   ·_𝑠 cvsca 17215  TopSetcts 17217  TopOpenctopn 17375  ∏_tcpt 17392   Σ_g cgsu 17394   mPwSer cmps 21894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-rel 5631  df-dm 5634  df-oprab 7364  df-mpo 7365  df-psr 21899

This theorem is referenced by:  psrbas  21923  psrelbas  21924  psrplusg  21926  psraddcl  21928  psrmulr  21931  psrmulcllem  21934  psrvscafval  21937  psrvscacl  21940  resspsrbas  21962  resspsradd  21963  resspsrmul  21964  mplval  21977  opsrle  22035  opsrbaslem  22037  psdval  22135  psdcl  22137  psdadd  22139  psdvsca  22140  psdmul  22142  psdpw  22146  psrbaspropd  22208  psropprmul  22211  mhmcopsr  43006