Theorem reldmpsr 21686

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 21681	. 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 7545	1 ⊢ Rel dom mPwSer

Syntax hints:   ∈ wcel 2104  {crab 3430  Vcvv 3472  ⦋csb 3892   ∪ cun 3945  {csn 4627  {ctp 4631  ⟨cop 4633   class class class wbr 5147   ↦ cmpt 5230   × cxp 5673  ^◡ccnv 5674  dom cdm 5675   ↾ cres 5677   “ cima 5678  Rel wrel 5680  ‘cfv 6542  (class class class)co 7411   ∈ cmpo 7413   ∘_f cof 7670   ∘_r cofr 7671   ↑_m cmap 8822  Fincfn 8941   ≤ cle 11253   − cmin 11448  ℕcn 12216  ℕ₀cn0 12476  ndxcnx 17130  Basecbs 17148  +_gcplusg 17201  ._rcmulr 17202  Scalarcsca 17204   ·_𝑠 cvsca 17205  TopSetcts 17207  TopOpenctopn 17371  ∏_tcpt 17388   Σ_g cgsu 17390   mPwSer cmps 21676

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-dm 5685  df-oprab 7415  df-mpo 7416  df-psr 21681

This theorem is referenced by:  psrbas  21716  psrelbas  21717  psrplusg  21719  psraddcl  21721  psrmulr  21722  psrmulcllem  21725  psrvscafval  21728  psrvscacl  21731  resspsrbas  21754  resspsradd  21755  resspsrmul  21756  mplval  21767  opsrle  21821  opsrbaslem  21823  opsrbaslemOLD  21824  psrbaspropd  21977  psropprmul  21980