Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-linds Unicode version

Definition df-linds 27277
Description: An independent set is a set which is independent as a family. See also islinds3 27304 and islinds4 27305. (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 27275 . 2  class LIndS
2 vw . . 3  set  w
3 cvv 2788 . . 3  class  _V
4 cid 4304 . . . . . 6  class  _I
5 vs . . . . . . 7  set  s
65cv 1622 . . . . . 6  class  s
74, 6cres 4691 . . . . 5  class  (  _I  |`  s )
82cv 1622 . . . . 5  class  w
9 clindf 27274 . . . . 5  class LIndF
107, 8, 9wbr 4023 . . . 4  wff  (  _I  |`  s ) LIndF  w
11 cbs 13148 . . . . . 6  class  Base
128, 11cfv 5255 . . . . 5  class  ( Base `  w )
1312cpw 3625 . . . 4  class  ~P ( Base `  w )
1410, 5, 13crab 2547 . . 3  class  { s  e.  ~P ( Base `  w )  |  (  _I  |`  s ) LIndF  w }
152, 3, 14cmpt 4077 . 2  class  ( w  e.  _V  |->  { s  e.  ~P ( Base `  w )  |  (  _I  |`  s ) LIndF  w } )
161, 15wceq 1623 1  wff LIndS  =  ( w  e.  _V  |->  { s  e.  ~P ( Base `  w )  |  (  _I  |`  s
) LIndF  w } )
Colors of variables: wff set class
This definition is referenced by:  islinds  27279
  Copyright terms: Public domain W3C validator