This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ Rel LIndF$

Step	Hyp	Ref	Expression
1		df-lindf	$⊢ LIndF = \{⟨f, w⟩ \| (f : dom f ⟶ {Base}_{w} \land \underset{˙}{[} Scalar (w) / s \underset{˙}{]} \forall x \in dom f \forall k \in ({Base}_{s} ∖ \{0_{s}\}) \neg k \cdot_{w} f (x) \in LSpan (w) (f [dom f ∖ \{x\}]))\}$
2	1	relopabiv	$⊢ Rel LIndF$