Theorem reldmfrlm

Description: The domain of the free module function is a relation. (Contributed by SN, 24-Sep-2026)

	Ref	Expression
Assertion	reldmfrlm	⊢ Rel dom freeLMod

Proof

Step	Hyp	Ref	Expression
1		df-frlm	⊢ freeLMod = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( 𝑟 ⊕m ( 𝑖 × { ( ringLMod ‘ 𝑟 ) } ) ) )
2	1	reldmmpo	⊢ Rel dom freeLMod