MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-linds Structured version   Visualization version   GIF version

Definition df-linds 19907
Description: An independent set is a set which is independent as a family. See also islinds3 19934 and islinds4 19935. (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
StepHypRef Expression
1 clinds 19905 . 2 class LIndS
2 vw . . 3 setvar 𝑤
3 cvv 3172 . . 3 class V
4 cid 4938 . . . . . 6 class I
5 vs . . . . . . 7 setvar 𝑠
65cv 1473 . . . . . 6 class 𝑠
74, 6cres 5030 . . . . 5 class ( I ↾ 𝑠)
82cv 1473 . . . . 5 class 𝑤
9 clindf 19904 . . . . 5 class LIndF
107, 8, 9wbr 4577 . . . 4 wff ( I ↾ 𝑠) LIndF 𝑤
11 cbs 15641 . . . . . 6 class Base
128, 11cfv 5790 . . . . 5 class (Base‘𝑤)
1312cpw 4107 . . . 4 class 𝒫 (Base‘𝑤)
1410, 5, 13crab 2899 . . 3 class {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ( I ↾ 𝑠) LIndF 𝑤}
152, 3, 14cmpt 4637 . 2 class (𝑤 ∈ V ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ( I ↾ 𝑠) LIndF 𝑤})
161, 15wceq 1474 1 wff LIndS = (𝑤 ∈ V ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ ( I ↾ 𝑠) LIndF 𝑤})
Colors of variables: wff setvar class
This definition is referenced by:  islinds  19909
  Copyright terms: Public domain W3C validator