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 = ( 𝑤 ∈ V ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑤 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clinds	⊢ LIndS
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		cbs	⊢ Base
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( Base ‘ 𝑤 )
7	6	cpw	⊢ 𝒫 ( Base ‘ 𝑤 )
8		cid	⊢ I
9	3	cv	⊢ 𝑠
10	8 9	cres	⊢ ( I ↾ 𝑠 )
11		clindf	⊢ LIndF
12	10 5 11	wbr	⊢ ( I ↾ 𝑠 ) LIndF 𝑤
13	12 3 7	crab	⊢ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑤 }
14	1 2 13	cmpt	⊢ ( 𝑤 ∈ V ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑤 } )
15	0 14	wceq	⊢ LIndS = ( 𝑤 ∈ V ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑤 } )