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	$$⊢\mathrm{LIndS}=\left(w\in \mathrm{V}⟼\left\{s\in 𝒫{\mathrm{Base}}_w|\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}w\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clinds	$$class\mathrm{LIndS}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class{\mathrm{Base}}_w$$
7	6	cpw	$$class𝒫{\mathrm{Base}}_w$$
8		cid	$$class\mathrm{I}$$
9	3	cv	$$setvars$$
10	8 9	cres	$$class\left({\mathrm{I}\upharpoonright }_s\right)$$
11		clindf	$$class\mathrm{LIndF}$$
12	10 5 11	wbr	$$wff\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}w$$
13	12 3 7	crab	$$class\left\{s\in 𝒫{\mathrm{Base}}_w|\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}w\right\}$$
14	1 2 13	cmpt	$$class\left(w\in \mathrm{V}⟼\left\{s\in 𝒫{\mathrm{Base}}_w|\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}w\right\}\right)$$
15	0 14	wceq	$$wff\mathrm{LIndS}=\left(w\in \mathrm{V}⟼\left\{s\in 𝒫{\mathrm{Base}}_w|\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}w\right\}\right)$$