Theorem reldmpsr 22043

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 22038	. 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 7544	1 ⊢ Rel dom mPwSer

Syntax hints:   ∈ wcel 2141  {crab 3414  Vcvv 3453  ⦋csb 3852   ∪ cun 3902  {csn 4588  {ctp 4592  ⟨cop 4594   class class class wbr 5108   ↦ cmpt 5191   × cxp 5659  ^◡ccnv 5660  dom cdm 5661   ↾ cres 5663   “ cima 5664  Rel wrel 5666  ‘cfv 6536  (class class class)co 7410   ∈ cmpo 7412   ∘_f cof 7672   ∘_r cofr 7673   ↑_m cmap 8823  Fincfn 8942   ≤ cle 11243   − cmin 11440  ℕcn 12232  ℕ₀cn0 12503  ndxcnx 17252  Basecbs 17268  +_gcplusg 17309  ._rcmulr 17310  Scalarcsca 17312   ·_𝑠 cvsca 17313  TopSetcts 17315  TopOpenctopn 17473  ∏_tcpt 17490   Σ_g cgsu 17492   mPwSer cmps 22033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rab 3415  df-v 3455  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 5667  df-rel 5668  df-dm 5671  df-oprab 7414  df-mpo 7415  df-psr 22038

This theorem is referenced by:  psrbas  22063  psrelbas  22064  psrplusg  22066  psraddcl  22068  psrmulr  22071  psrmulcllem  22074  psrvscafval  22077  psrvscacl  22080  resspsrbas  22102  resspsradd  22103  resspsrmul  22104  mplval  22117  opsrle  22177  opsrbaslem  22179  psdval  22301  psdcl  22303  psdadd  22305  psdvsca  22306  psdmul  22308  psdpw  22312  psrbaspropd  22373  psropprmul  22376  mhmcopsr  43260