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	$$⊢\mathrm{Rel}\mathrm{linIndS}$$

Proof

Step	Hyp	Ref	Expression
1		df-lininds	$$⊢\mathrm{linIndS}=\left\{⟨s,m⟩|\left(s\in 𝒫{\mathrm{Base}}_m\wedge \forall f\in \left({{\mathrm{Base}}_{\mathrm{Scalar}\left(m\right)}}^s\right)\left(\left({finSupp}_{0_{\mathrm{Scalar}\left(m\right)}}\left(f\right)\wedge f\mathrm{linC}\left(m\right)s=0_m\right)\to \forall x\in sf\left(x\right)=0_{\mathrm{Scalar}\left(m\right)}\right)\right)\right\}$$
2	1	relopabiv	$$⊢\mathrm{Rel}\mathrm{linIndS}$$