Step |
Hyp |
Ref |
Expression |
1 |
|
islinds.b |
⊢ 𝐵 = ( Base ‘ 𝑊 ) |
2 |
|
elex |
⊢ ( 𝑊 ∈ 𝑉 → 𝑊 ∈ V ) |
3 |
|
fveq2 |
⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) ) |
4 |
3
|
pweqd |
⊢ ( 𝑤 = 𝑊 → 𝒫 ( Base ‘ 𝑤 ) = 𝒫 ( Base ‘ 𝑊 ) ) |
5 |
|
breq2 |
⊢ ( 𝑤 = 𝑊 → ( ( I ↾ 𝑠 ) LIndF 𝑤 ↔ ( I ↾ 𝑠 ) LIndF 𝑊 ) ) |
6 |
4 5
|
rabeqbidv |
⊢ ( 𝑤 = 𝑊 → { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑤 } = { 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑊 } ) |
7 |
|
df-linds |
⊢ LIndS = ( 𝑤 ∈ V ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑤 } ) |
8 |
|
fvex |
⊢ ( Base ‘ 𝑊 ) ∈ V |
9 |
8
|
pwex |
⊢ 𝒫 ( Base ‘ 𝑊 ) ∈ V |
10 |
9
|
rabex |
⊢ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑊 } ∈ V |
11 |
6 7 10
|
fvmpt |
⊢ ( 𝑊 ∈ V → ( LIndS ‘ 𝑊 ) = { 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑊 } ) |
12 |
2 11
|
syl |
⊢ ( 𝑊 ∈ 𝑉 → ( LIndS ‘ 𝑊 ) = { 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑊 } ) |
13 |
12
|
eleq2d |
⊢ ( 𝑊 ∈ 𝑉 → ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ↔ 𝑋 ∈ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑊 } ) ) |
14 |
|
reseq2 |
⊢ ( 𝑠 = 𝑋 → ( I ↾ 𝑠 ) = ( I ↾ 𝑋 ) ) |
15 |
14
|
breq1d |
⊢ ( 𝑠 = 𝑋 → ( ( I ↾ 𝑠 ) LIndF 𝑊 ↔ ( I ↾ 𝑋 ) LIndF 𝑊 ) ) |
16 |
15
|
elrab |
⊢ ( 𝑋 ∈ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑊 } ↔ ( 𝑋 ∈ 𝒫 ( Base ‘ 𝑊 ) ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) ) |
17 |
13 16
|
bitrdi |
⊢ ( 𝑊 ∈ 𝑉 → ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑋 ∈ 𝒫 ( Base ‘ 𝑊 ) ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) ) ) |
18 |
8
|
elpw2 |
⊢ ( 𝑋 ∈ 𝒫 ( Base ‘ 𝑊 ) ↔ 𝑋 ⊆ ( Base ‘ 𝑊 ) ) |
19 |
1
|
sseq2i |
⊢ ( 𝑋 ⊆ 𝐵 ↔ 𝑋 ⊆ ( Base ‘ 𝑊 ) ) |
20 |
18 19
|
bitr4i |
⊢ ( 𝑋 ∈ 𝒫 ( Base ‘ 𝑊 ) ↔ 𝑋 ⊆ 𝐵 ) |
21 |
20
|
anbi1i |
⊢ ( ( 𝑋 ∈ 𝒫 ( Base ‘ 𝑊 ) ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) ↔ ( 𝑋 ⊆ 𝐵 ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) ) |
22 |
17 21
|
bitrdi |
⊢ ( 𝑊 ∈ 𝑉 → ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑋 ⊆ 𝐵 ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) ) ) |