MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-linds Structured version   Unicode version

Definition df-linds 18356
Description: An independent set is a set which is independent as a family. See also islinds3 18383 and islinds4 18384. (Contributed by Stefan O'Rear, 24-Feb-2015.)
Assertion
Ref Expression
df-linds  |- LIndS  =  ( w  e.  _V  |->  { s  e.  ~P ( Base `  w )  |  (  _I  |`  s
) LIndF  w } )
Distinct variable group:    w, s

Detailed syntax breakdown of Definition df-linds
StepHypRef Expression
1 clinds 18354 . 2  class LIndS
2 vw . . 3  setvar  w
3 cvv 3072 . . 3  class  _V
4 cid 4734 . . . . . 6  class  _I
5 vs . . . . . . 7  setvar  s
65cv 1369 . . . . . 6  class  s
74, 6cres 4945 . . . . 5  class  (  _I  |`  s )
82cv 1369 . . . . 5  class  w
9 clindf 18353 . . . . 5  class LIndF
107, 8, 9wbr 4395 . . . 4  wff  (  _I  |`  s ) LIndF  w
11 cbs 14287 . . . . . 6  class  Base
128, 11cfv 5521 . . . . 5  class  ( Base `  w )
1312cpw 3963 . . . 4  class  ~P ( Base `  w )
1410, 5, 13crab 2800 . . 3  class  { s  e.  ~P ( Base `  w )  |  (  _I  |`  s ) LIndF  w }
152, 3, 14cmpt 4453 . 2  class  ( w  e.  _V  |->  { s  e.  ~P ( Base `  w )  |  (  _I  |`  s ) LIndF  w } )
161, 15wceq 1370 1  wff LIndS  =  ( w  e.  _V  |->  { s  e.  ~P ( Base `  w )  |  (  _I  |`  s
) LIndF  w } )
Colors of variables: wff setvar class
This definition is referenced by:  islinds  18358
  Copyright terms: Public domain W3C validator