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 = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑠 Xs 𝑟 ) ↾s { 𝑓 ∈ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∣ { 𝑥 ∈ dom 𝑟 ∣ ( 𝑓 ‘ 𝑥 ) ≠ ( 0g ‘ ( 𝑟 ‘ 𝑥 ) ) } ∈ Fin } ) )
2	1	reldmmpo	⊢ Rel dom ⊕m