Theorem reldmpsr 21839

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 21834	. 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 7487	1 ⊢ Rel dom mPwSer

Syntax hints:   ∈ wcel 2109  {crab 3396  Vcvv 3438  ⦋csb 3853   ∪ cun 3903  {csn 4579  {ctp 4583  ⟨cop 4585   class class class wbr 5095   ↦ cmpt 5176   × cxp 5621  ^◡ccnv 5622  dom cdm 5623   ↾ cres 5625   “ cima 5626  Rel wrel 5628  ‘cfv 6486  (class class class)co 7353   ∈ cmpo 7355   ∘_f cof 7615   ∘_r cofr 7616   ↑_m cmap 8760  Fincfn 8879   ≤ cle 11169   − cmin 11365  ℕcn 12146  ℕ₀cn0 12402  ndxcnx 17122  Basecbs 17138  +_gcplusg 17179  ._rcmulr 17180  Scalarcsca 17182   ·_𝑠 cvsca 17183  TopSetcts 17185  TopOpenctopn 17343  ∏_tcpt 17360   Σ_g cgsu 17362   mPwSer cmps 21829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-rel 5630  df-dm 5633  df-oprab 7357  df-mpo 7358  df-psr 21834

This theorem is referenced by:  psrbas  21858  psrelbas  21859  psrplusg  21861  psraddcl  21863  psraddclOLD  21864  psrmulr  21867  psrmulcllem  21870  psrvscafval  21873  psrvscacl  21876  resspsrbas  21899  resspsradd  21900  resspsrmul  21901  mplval  21914  opsrle  21970  opsrbaslem  21972  psdval  22062  psdcl  22064  psdadd  22066  psdvsca  22067  psdmul  22069  psdpw  22073  psrbaspropd  22135  psropprmul  22138  mhmcopsr  42522