This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reldmdsmm

Description: The direct sum is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015)

Ref Expression
Assertion reldmdsmm ⊢ Rel ⁡ dom ⁡ ⊕ m

Proof

Step Hyp Ref Expression
1 df-dsmm ⊢ ⊕ m = s ∈ V , r ∈ V ⟼ s ⨉ 𝑠 r ↾ 𝑠 f ∈ ⨉ x ∈ dom ⁡ r Base r ⁡ x | x ∈ dom ⁡ r | f ⁡ x ≠ 0 r ⁡ x ∈ Fin
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ ⊕ m