Theorem reldmpsr 21892

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 21887	. 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 7493	1 ⊢ Rel dom mPwSer

Syntax hints:   ∈ wcel 2121  {crab 3393  Vcvv 3433  ⦋csb 3832   ∪ cun 3882  {csn 4557  {ctp 4561  ⟨cop 4563   class class class wbr 5074   ↦ cmpt 5155   × cxp 5618  ^◡ccnv 5619  dom cdm 5620   ↾ cres 5622   “ cima 5623  Rel wrel 5625  ‘cfv 6488  (class class class)co 7359   ∈ cmpo 7361   ∘_f cof 7621   ∘_r cofr 7622   ↑_m cmap 8767  Fincfn 8887   ≤ cle 11176   − cmin 11373  ℕcn 12169  ℕ₀cn0 12432  ndxcnx 17158  Basecbs 17174  +_gcplusg 17215  ._rcmulr 17216  Scalarcsca 17218   ·_𝑠 cvsca 17219  TopSetcts 17221  TopOpenctopn 17379  ∏_tcpt 17396   Σ_g cgsu 17398   mPwSer cmps 21882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5220  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-xp 5626  df-rel 5627  df-dm 5630  df-oprab 7363  df-mpo 7364  df-psr 21887

This theorem is referenced by:  psrbas  21912  psrelbas  21913  psrplusg  21915  psraddcl  21917  psrmulr  21920  psrmulcllem  21923  psrvscafval  21926  psrvscacl  21929  resspsrbas  21951  resspsradd  21952  resspsrmul  21953  mplval  21966  opsrle  22026  opsrbaslem  22028  psdval  22150  psdcl  22152  psdadd  22154  psdvsca  22155  psdmul  22157  psdpw  22161  psrbaspropd  22222  psropprmul  22225  mhmcopsr  43043