This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑤 } )