MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rellindf Structured version   Visualization version   GIF version

Theorem rellindf 20364
Description: The independent-family predicate is a proper relation and can be used with brrelexi 5297. (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.
StepHypRef Expression
1 df-lindf 20362 . 2 LIndF = {⟨𝑓, 𝑤⟩ ∣ (𝑓:dom 𝑓⟶(Base‘𝑤) ∧ [(Scalar‘𝑤) / 𝑠]𝑥 ∈ dom 𝑓𝑘 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑘( ·𝑠𝑤)(𝑓𝑥)) ∈ ((LSpan‘𝑤)‘(𝑓 “ (dom 𝑓 ∖ {𝑥}))))}
21relopabi 5383 1 Rel LIndF
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 382  wcel 2145  wral 3061  [wsbc 3587  cdif 3720  {csn 4317  dom cdm 5250  cima 5253  Rel wrel 5255  wf 6026  cfv 6030  (class class class)co 6796  Basecbs 16064  Scalarcsca 16152   ·𝑠 cvsca 16153  0gc0g 16308  LSpanclspn 19184   LIndF clindf 20360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-opab 4848  df-xp 5256  df-rel 5257  df-lindf 20362
This theorem is referenced by:  lindff  20371  lindfind  20372  f1lindf  20378  lindfmm  20383  lsslindf  20386
  Copyright terms: Public domain W3C validator