Theorem reldmpsr 22249

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 22244	. 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 7575	1 ⊢ Rel dom mPwSer

This proof depends on syntax axioms:   ∈ wcel 2147  {crab 3416  Vcvv 3454  ⦋csb 3851   ∪ cun 4152  {csn 4588  {ctp 4592  ⟨cop 4838   class class class wbr 5106   ↦ cmpt 5189   × cxp 5653  ^◡ccnv 5654  dom cdm 5655   ↾ cres 5657   “ cima 5658  Rel wrel 5660  ‘cfv 6555  (class class class)co 7440   ∈ cmpo 7442   ∘_f cof 7712   ∘_r cofr 7713   ↑_m cmap 8872  Fincfn 8998   ≤ cle 11368   − cmin 11565  ℕcn 12359  ℕ₀cn0 12630  ndxcnx 17397  Basecbs 17413  +_gcplusg 17454  ._rcmulr 17455  Scalarcsca 17457   ·_𝑠 cvsca 17458  TopSetcts 17460  TopOpenctopn 17618  ∏_tcpt 17635   Σ_g cgsu 17637   mPwSer cmps 22239

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662  df-dm 5665  df-oprab 7444  df-mpo 7445  df-psr 22244

This theorem is used by:  psrbas  22269  psrelbas  22270  psrplusg  22272  psraddcl  22274  psrmulr  22277  psrmulcllem  22280  psrvscafval  22283  psrvscacl  22286  resspsrbas  22308  resspsradd  22309  resspsrmul  22310  mplval  22323  opsrle  22383  opsrbaslem  22385  psdval  22507  psdcl  22509  psdadd  22511  psdvsca  22512  psdmul  22514  psdpw  22518  psrbaspropd  22579  psropprmul  22582  mhmcopsr  43799