Definition df-linds

Description: An independent set is a set which is independent as a family. See also islinds3 and islinds4 . (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Assertion	df-linds	|- LIndS = ( w e. _V |-> { s e. ~P ( Base ` w ) | ( _I |` s ) LIndF w } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clinds	|- LIndS
1		vw	|- w
2		cvv	|- _V
3		vs	|- s
4		cbs	|- Base
5	1	cv	|- w
6	5 4	cfv	|- ( Base ` w )
7	6	cpw	|- ~P ( Base ` w )
8		cid	|- _I
9	3	cv	|- s
10	8 9	cres	|- ( _I |` s )
11		clindf	|- LIndF
12	10 5 11	wbr	|- ( _I |` s ) LIndF w
13	12 3 7	crab	|- { s e. ~P ( Base ` w ) | ( _I |` s ) LIndF w }
14	1 2 13	cmpt	|- ( w e. _V |-> { s e. ~P ( Base ` w ) | ( _I |` s ) LIndF w } )
15	0 14	wceq	|- LIndS = ( w e. _V |-> { s e. ~P ( Base ` w ) | ( _I |` s ) LIndF w } )