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	$$⊢B={\mathrm{Base}}_W$$
Assertion	islinds	$$⊢W\in V\to \left(X\in \mathrm{LIndS}\left(W\right)\leftrightarrow \left(X\subseteq B\wedge \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		islinds.b	$$⊢B={\mathrm{Base}}_W$$
2		elex	$$⊢W\in V\to W\in \mathrm{V}$$
3		fveq2	$$⊢w=W\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
4	3	pweqd	$$⊢w=W\to 𝒫{\mathrm{Base}}_w=𝒫{\mathrm{Base}}_W$$
5		breq2	$$⊢w=W\to \left(\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}w\leftrightarrow \left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}W\right)$$
6	4 5	rabeqbidv	$$⊢w=W\to \left\{s\in 𝒫{\mathrm{Base}}_w|\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}w\right\}=\left\{s\in 𝒫{\mathrm{Base}}_W|\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}W\right\}$$
7		df-linds	$$⊢\mathrm{LIndS}=\left(w\in \mathrm{V}⟼\left\{s\in 𝒫{\mathrm{Base}}_w|\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}w\right\}\right)$$
8		fvex	$$⊢{\mathrm{Base}}_W\in \mathrm{V}$$
9	8	pwex	$$⊢𝒫{\mathrm{Base}}_W\in \mathrm{V}$$
10	9	rabex	$$⊢\left\{s\in 𝒫{\mathrm{Base}}_W|\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}W\right\}\in \mathrm{V}$$
11	6 7 10	fvmpt	$$⊢W\in \mathrm{V}\to \mathrm{LIndS}\left(W\right)=\left\{s\in 𝒫{\mathrm{Base}}_W|\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}W\right\}$$
12	2 11	syl	$$⊢W\in V\to \mathrm{LIndS}\left(W\right)=\left\{s\in 𝒫{\mathrm{Base}}_W|\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}W\right\}$$
13	12	eleq2d	$$⊢W\in V\to \left(X\in \mathrm{LIndS}\left(W\right)\leftrightarrow X\in \left\{s\in 𝒫{\mathrm{Base}}_W|\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}W\right\}\right)$$
14		reseq2	$$⊢s=X\to {\mathrm{I}\upharpoonright }_s={\mathrm{I}\upharpoonright }_X$$
15	14	breq1d	$$⊢s=X\to \left(\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}W\leftrightarrow \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W\right)$$
16	15	elrab	$$⊢X\in \left\{s\in 𝒫{\mathrm{Base}}_W|\left({\mathrm{I}\upharpoonright }_s\right)\mathrm{LIndF}W\right\}\leftrightarrow \left(X\in 𝒫{\mathrm{Base}}_W\wedge \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W\right)$$
17	13 16	bitrdi	$$⊢W\in V\to \left(X\in \mathrm{LIndS}\left(W\right)\leftrightarrow \left(X\in 𝒫{\mathrm{Base}}_W\wedge \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W\right)\right)$$
18	8	elpw2	$$⊢X\in 𝒫{\mathrm{Base}}_W\leftrightarrow X\subseteq {\mathrm{Base}}_W$$
19	1	sseq2i	$$⊢X\subseteq B\leftrightarrow X\subseteq {\mathrm{Base}}_W$$
20	18 19	bitr4i	$$⊢X\in 𝒫{\mathrm{Base}}_W\leftrightarrow X\subseteq B$$
21	20	anbi1i	$$⊢\left(X\in 𝒫{\mathrm{Base}}_W\wedge \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W\right)\leftrightarrow \left(X\subseteq B\wedge \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W\right)$$
22	17 21	bitrdi	$$⊢W\in V\to \left(X\in \mathrm{LIndS}\left(W\right)\leftrightarrow \left(X\subseteq B\wedge \left({\mathrm{I}\upharpoonright }_X\right)\mathrm{LIndF}W\right)\right)$$