Theorem rellininds

Description: The class defining the relation between a module and its linearly independent subsets is a relation. (Contributed by AV, 13-Apr-2019)

	Ref	Expression
Assertion	rellininds	⊢ Rel linIndS

Proof

Step	Hyp	Ref	Expression
1		df-lininds	⊢ linIndS = { ⟨ 𝑠 , 𝑚 ⟩ ∣ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ∧ ∀ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑠 ) ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ∧ ( 𝑓 ( linC ‘ 𝑚 ) 𝑠 ) = ( 0g ‘ 𝑚 ) ) → ∀ 𝑥 ∈ 𝑠 ( 𝑓 ‘ 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑚 ) ) ) ) }
2	1	relopabiv	⊢ Rel linIndS