Theorem rellindf 21347

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

Assertion

Ref	Expression
rellindf	⊢ Rel LIndF

Proof of Theorem rellindf

Dummy variables 𝑓 𝑘 𝑠 𝑤 𝑥 are mutually distinct and distinct from all other variables.

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

Syntax hints:  ¬ wn 3   ∧ wa 397   ∈ wcel 2107  ∀wral 3062  [wsbc 3776   ∖ cdif 3944  {csn 4627  dom cdm 5675   “ cima 5678  Rel wrel 5680  ⟶wf 6536  ‘cfv 6540  (class class class)co 7404  Basecbs 17140  Scalarcsca 17196   ·_𝑠 cvsca 17197  0_gc0g 17381  LSpanclspn 20570   LIndF clindf 21343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3954  df-ss 3964  df-opab 5210  df-xp 5681  df-rel 5682  df-lindf 21345

This theorem is referenced by:  lindff  21354  lindfind  21355  f1lindf  21361  lindfmm  21366  lsslindf  21369