Theorem reldmpsr 21882

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 21877	. 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 7502	1 ⊢ Rel dom mPwSer

Syntax hints:   ∈ wcel 2114  {crab 3401  Vcvv 3442  ⦋csb 3851   ∪ cun 3901  {csn 4582  {ctp 4586  ⟨cop 4588   class class class wbr 5100   ↦ cmpt 5181   × cxp 5630  ^◡ccnv 5631  dom cdm 5632   ↾ cres 5634   “ cima 5635  Rel wrel 5637  ‘cfv 6500  (class class class)co 7368   ∈ cmpo 7370   ∘_f cof 7630   ∘_r cofr 7631   ↑_m cmap 8775  Fincfn 8895   ≤ cle 11179   − cmin 11376  ℕcn 12157  ℕ₀cn0 12413  ndxcnx 17132  Basecbs 17148  +_gcplusg 17189  ._rcmulr 17190  Scalarcsca 17192   ·_𝑠 cvsca 17193  TopSetcts 17195  TopOpenctopn 17353  ∏_tcpt 17370   Σ_g cgsu 17372   mPwSer cmps 21872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-dm 5642  df-oprab 7372  df-mpo 7373  df-psr 21877

This theorem is referenced by:  psrbas  21901  psrelbas  21902  psrplusg  21904  psraddcl  21906  psraddclOLD  21907  psrmulr  21910  psrmulcllem  21913  psrvscafval  21916  psrvscacl  21919  resspsrbas  21941  resspsradd  21942  resspsrmul  21943  mplval  21956  opsrle  22014  opsrbaslem  22016  psdval  22114  psdcl  22116  psdadd  22118  psdvsca  22119  psdmul  22121  psdpw  22125  psrbaspropd  22187  psropprmul  22190  mhmcopsr  42911