Definition df-linds 21662

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

Assertion

Ref	Expression
df-linds	⊢ LIndS = (𝑤 ∈ V ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ( I ↾ 𝑠) LIndF 𝑤})

Distinct variable group:   𝑤,𝑠

Detailed syntax breakdown of Definition df-linds

Step	Hyp	Ref	Expression
1		clinds 21660	. 2 class LIndS
2		vw	. . 3 setvar 𝑤
3		cvv 3466	. . 3 class V
4		cid 5563	. . . . . 6 class I
5		vs	. . . . . . 7 setvar 𝑠
6	5	cv 1532	. . . . . 6 class 𝑠
7	4, 6	cres 5668	. . . . 5 class ( I ↾ 𝑠)
8	2	cv 1532	. . . . 5 class 𝑤
9		clindf 21659	. . . . 5 class LIndF
10	7, 8, 9	wbr 5138	. . . 4 wff ( I ↾ 𝑠) LIndF 𝑤
11		cbs 17140	. . . . . 6 class Base
12	8, 11	cfv 6533	. . . . 5 class (Base‘𝑤)
13	12	cpw 4594	. . . 4 class 𝒫 (Base‘𝑤)
14	10, 5, 13	crab 3424	. . 3 class {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ( I ↾ 𝑠) LIndF 𝑤}
15	2, 3, 14	cmpt 5221	. 2 class (𝑤 ∈ V ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ( I ↾ 𝑠) LIndF 𝑤})
16	1, 15	wceq 1533	1 wff LIndS = (𝑤 ∈ V ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ( I ↾ 𝑠) LIndF 𝑤})

This definition is referenced by:  islinds  21664