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

Proof

Step	Hyp	Ref	Expression
1		df-lindf	\|- LIndF = { <. f , w >. \| ( f : dom f --> ( Base ` w ) /\ [. ( Scalar ` w ) / s ]. A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) ) }
2	1	relopabiv	\|- Rel LIndF

Step

Hyp

Ref

Expression

df-lindf

 |-  LIndF = { <. f , w >. | ( f : dom f --> ( Base ` w ) /\ [. ( Scalar ` w ) / s ]. A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) ) ) }

relopabiv

 |-  Rel LIndF