Definition df-linds 20146

Description: An independent set is a set which is independent as a family. See also islinds3 20173 and islinds4 20174. (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

Step	Hyp	Ref	Expression
1		clinds 20144	. 2 class LIndS
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		cid 5023	. . . . . 6 class _I
5		vs	. . . . . . 7 setvar s
6	5	cv 1482	. . . . . 6 class s
7	4, 6	cres 5116	. . . . 5 class ( _I |` s )
8	2	cv 1482	. . . . 5 class w
9		clindf 20143	. . . . 5 class LIndF
10	7, 8, 9	wbr 4653	. . . 4 wff ( _I |` s ) LIndF w
11		cbs 15857	. . . . . 6 class Base
12	8, 11	cfv 5888	. . . . 5 class ( Base ` w )
13	12	cpw 4158	. . . 4 class ~P ( Base ` w )
14	10, 5, 13	crab 2916	. . 3 class { s e. ~P ( Base ` w ) | ( _I |` s ) LIndF w }
15	2, 3, 14	cmpt 4729	. 2 class ( w e. _V |-> { s e. ~P ( Base ` w ) | ( _I |` s ) LIndF w } )
16	1, 15	wceq 1483	1 wff LIndS = ( w e. _V |-> { s e. ~P ( Base ` w ) | ( _I |` s ) LIndF w } )

This definition is referenced by:  islinds  20148