Theorem reldmpsr 22222

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 22217	. 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 7554	1 ⊢ Rel dom mPwSer

This proof depends on syntax axioms:   ∈ wcel 2144  {crab 3412  Vcvv 3450  ⦋csb 3846   ∪ cun 4149  {csn 4583  {ctp 4587  ⟨cop 4589   class class class wbr 5102   ↦ cmpt 5185   × cxp 5648  ^◡ccnv 5649  dom cdm 5650   ↾ cres 5652   “ cima 5653  Rel wrel 5655  ‘cfv 6538  (class class class)co 7420   ∈ cmpo 7422   ∘_f cof 7691   ∘_r cofr 7692   ↑_m cmap 8847  Fincfn 8973   ≤ cle 11344   − cmin 11541  ℕcn 12335  ℕ₀cn0 12606  ndxcnx 17371  Basecbs 17387  +_gcplusg 17428  ._rcmulr 17429  Scalarcsca 17431   ·_𝑠 cvsca 17432  TopSetcts 17434  TopOpenctopn 17592  ∏_tcpt 17609   Σ_g cgsu 17611   mPwSer cmps 22212

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-dm 5660  df-oprab 7424  df-mpo 7425  df-psr 22217

This theorem is used by:  psrbas  22242  psrelbas  22243  psrplusg  22245  psraddcl  22247  psrmulr  22250  psrmulcllem  22253  psrvscafval  22256  psrvscacl  22259  resspsrbas  22281  resspsradd  22282  resspsrmul  22283  mplval  22296  opsrle  22356  opsrbaslem  22358  psdval  22480  psdcl  22482  psdadd  22484  psdvsca  22485  psdmul  22487  psdpw  22491  psrbaspropd  22552  psropprmul  22555  mhmcopsr  43609