Theorem rellindf

Description: The independent-family predicate is a proper relation and can be used with brrelex1i . (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Assertion	rellindf	$$⊢\mathrm{Rel}\mathrm{LIndF}$$

Proof

Step	Hyp	Ref	Expression
1		df-lindf	$$⊢\mathrm{LIndF}=\left\{⟨f,w⟩|\left(f:\mathrm{dom}f⟶{\mathrm{Base}}_w\wedge \underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\right)\right\}$$
2	1	relopabi	$$⊢\mathrm{Rel}\mathrm{LIndF}$$