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

Proof

Step	Hyp	Ref	Expression
1		df-lindf	⊢ LIndF = { ⟨ 𝑓 , 𝑤 ⟩ ∣ ( 𝑓 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ∧ [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ) }
2	1	relopabiv	⊢ Rel LIndF