Theorem reldmpsr 22075

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 22070	. 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 7546	1 ⊢ Rel dom mPwSer

This proof depends on syntax axioms:   ∈ wcel 2142  {crab 3415  Vcvv 3454  ⦋csb 3852   ∪ cun 3902  {csn 4588  {ctp 4592  ⟨cop 4594   class class class wbr 5108   ↦ cmpt 5191   × cxp 5658  ^◡ccnv 5659  dom cdm 5660   ↾ cres 5662   “ cima 5663  Rel wrel 5665  ‘cfv 6536  (class class class)co 7412   ∈ cmpo 7414   ∘_f cof 7674   ∘_r cofr 7675   ↑_m cmap 8822  Fincfn 8941   ≤ cle 11250   − cmin 11447  ℕcn 12239  ℕ₀cn0 12510  ndxcnx 17259  Basecbs 17275  +_gcplusg 17316  ._rcmulr 17317  Scalarcsca 17319   ·_𝑠 cvsca 17320  TopSetcts 17322  TopOpenctopn 17480  ∏_tcpt 17497   Σ_g cgsu 17499   mPwSer cmps 22065

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-xp 5666  df-rel 5667  df-dm 5670  df-oprab 7416  df-mpo 7417  df-psr 22070

This theorem is used by:  psrbas  22095  psrelbas  22096  psrplusg  22098  psraddcl  22100  psrmulr  22103  psrmulcllem  22106  psrvscafval  22109  psrvscacl  22112  resspsrbas  22134  resspsradd  22135  resspsrmul  22136  mplval  22149  opsrle  22209  opsrbaslem  22211  psdval  22333  psdcl  22335  psdadd  22337  psdvsca  22338  psdmul  22340  psdpw  22344  psrbaspropd  22405  psropprmul  22408  mhmcopsr  43340