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 27380
Description: An independent set is a set which is independent as a family. See also islinds3 27407 and islinds4 27408. (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 27378 . 2  class LIndS
2 vw . . 3  set  w
3 cvv 2801 . . 3  class  _V
4 cid 4320 . . . . . 6  class  _I
5 vs . . . . . . 7  set  s
65cv 1631 . . . . . 6  class  s
74, 6cres 4707 . . . . 5  class  (  _I  |`  s )
82cv 1631 . . . . 5  class  w
9 clindf 27377 . . . . 5  class LIndF
107, 8, 9wbr 4039 . . . 4  wff  (  _I  |`  s ) LIndF  w
11 cbs 13164 . . . . . 6  class  Base
128, 11cfv 5271 . . . . 5  class  ( Base `  w )
1312cpw 3638 . . . 4  class  ~P ( Base `  w )
1410, 5, 13crab 2560 . . 3  class  { s  e.  ~P ( Base `  w )  |  (  _I  |`  s ) LIndF  w }
152, 3, 14cmpt 4093 . 2  class  ( w  e.  _V  |->  { s  e.  ~P ( Base `  w )  |  (  _I  |`  s ) LIndF  w } )
161, 15wceq 1632 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  27382
  Copyright terms: Public domain W3C validator