Theorem islinds

Description: Property of an independent set of vectors in terms of an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Hypothesis	islinds.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion	islinds	⊢ ( 𝑊 ∈ 𝑉 → ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑋 ⊆ 𝐵 ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) ) )

Proof

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 𝑊 ) ) )