Theorem reldmpsr 21879

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 21874	. 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

Syntax hints:   ∈ wcel 2109  {crab 3420  Vcvv 3464  ⦋csb 3879   ∪ cun 3929  {csn 4606  {ctp 4610  ⟨cop 4612   class class class wbr 5124   ↦ cmpt 5206   × cxp 5657  ^◡ccnv 5658  dom cdm 5659   ↾ cres 5661   “ cima 5662  Rel wrel 5664  ‘cfv 6536  (class class class)co 7410   ∈ cmpo 7412   ∘_f cof 7674   ∘_r cofr 7675   ↑_m cmap 8845  Fincfn 8964   ≤ cle 11275   − cmin 11471  ℕcn 12245  ℕ₀cn0 12506  ndxcnx 17217  Basecbs 17233  +_gcplusg 17276  ._rcmulr 17277  Scalarcsca 17279   ·_𝑠 cvsca 17280  TopSetcts 17282  TopOpenctopn 17440  ∏_tcpt 17457   Σ_g cgsu 17459   mPwSer cmps 21869

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-xp 5665  df-rel 5666  df-dm 5669  df-oprab 7414  df-mpo 7415  df-psr 21874

This theorem is referenced by:  psrbas  21898  psrelbas  21899  psrplusg  21901  psraddcl  21903  psraddclOLD  21904  psrmulr  21907  psrmulcllem  21910  psrvscafval  21913  psrvscacl  21916  resspsrbas  21939  resspsradd  21940  resspsrmul  21941  mplval  21954  opsrle  22010  opsrbaslem  22012  psdval  22102  psdcl  22104  psdadd  22106  psdvsca  22107  psdmul  22109  psdpw  22113  psrbaspropd  22175  psropprmul  22178  mhmcopsr  42539