Theorem reldmpsr

Description: The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Assertion	reldmpsr	⊢ Rel dom mPwSer

Proof

Step	Hyp	Ref	Expression
1		df-psr	⊢ 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	⊢ Rel dom mPwSer