Theorem reldmpsr 21870

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 21865	. 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 7492	1 ⊢ Rel dom mPwSer

Syntax hints:   ∈ wcel 2113  {crab 3399  Vcvv 3440  ⦋csb 3849   ∪ cun 3899  {csn 4580  {ctp 4584  ⟨cop 4586   class class class wbr 5098   ↦ cmpt 5179   × cxp 5622  ^◡ccnv 5623  dom cdm 5624   ↾ cres 5626   “ cima 5627  Rel wrel 5629  ‘cfv 6492  (class class class)co 7358   ∈ cmpo 7360   ∘_f cof 7620   ∘_r cofr 7621   ↑_m cmap 8763  Fincfn 8883   ≤ cle 11167   − cmin 11364  ℕcn 12145  ℕ₀cn0 12401  ndxcnx 17120  Basecbs 17136  +_gcplusg 17177  ._rcmulr 17178  Scalarcsca 17180   ·_𝑠 cvsca 17181  TopSetcts 17183  TopOpenctopn 17341  ∏_tcpt 17358   Σ_g cgsu 17360   mPwSer cmps 21860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-dm 5634  df-oprab 7362  df-mpo 7363  df-psr 21865

This theorem is referenced by:  psrbas  21889  psrelbas  21890  psrplusg  21892  psraddcl  21894  psraddclOLD  21895  psrmulr  21898  psrmulcllem  21901  psrvscafval  21904  psrvscacl  21907  resspsrbas  21929  resspsradd  21930  resspsrmul  21931  mplval  21944  opsrle  22002  opsrbaslem  22004  psdval  22102  psdcl  22104  psdadd  22106  psdvsca  22107  psdmul  22109  psdpw  22113  psrbaspropd  22175  psropprmul  22178  mhmcopsr  42798