Theorem reldmpsr 22169

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 22164	. 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 7543	1 ⊢ Rel dom mPwSer

This proof depends on syntax axioms:   ∈ wcel 2145  {crab 3412  Vcvv 3450  ⦋csb 3847   ∪ cun 3897  {csn 4584  {ctp 4588  ⟨cop 4590   class class class wbr 5103   ↦ cmpt 5186   × cxp 5646  ^◡ccnv 5647  dom cdm 5648   ↾ cres 5650   “ cima 5651  Rel wrel 5653  ‘cfv 6528  (class class class)co 7409   ∈ cmpo 7411   ∘_f cof 7675   ∘_r cofr 7676   ↑_m cmap 8826  Fincfn 8952   ≤ cle 11301   − cmin 11498  ℕcn 12290  ℕ₀cn0 12561  ndxcnx 17318  Basecbs 17334  +_gcplusg 17375  ._rcmulr 17376  Scalarcsca 17378   ·_𝑠 cvsca 17379  TopSetcts 17381  TopOpenctopn 17539  ∏_tcpt 17556   Σ_g cgsu 17558   mPwSer cmps 22159

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-pr 5391

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5654  df-rel 5655  df-dm 5658  df-oprab 7413  df-mpo 7414  df-psr 22164

This theorem is used by:  psrbas  22189  psrelbas  22190  psrplusg  22192  psraddcl  22194  psrmulr  22197  psrmulcllem  22200  psrvscafval  22203  psrvscacl  22206  resspsrbas  22228  resspsradd  22229  resspsrmul  22230  mplval  22243  opsrle  22303  opsrbaslem  22305  psdval  22427  psdcl  22429  psdadd  22431  psdvsca  22432  psdmul  22434  psdpw  22438  psrbaspropd  22499  psropprmul  22502  mhmcopsr  43524