Theorem lbsextlem1

Description: Lemma for lbsext . The set S is the set of all linearly independent sets containing C ; we show here that it is nonempty. (Contributed by Mario Carneiro, 25-Jun-2014)

	Ref	Expression
Hypotheses	lbsext.v	$$⊢V={\mathrm{Base}}_W$$
	lbsext.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
	lbsext.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lbsext.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lbsext.c	$$⊢\phi \to C\subseteq V$$
	lbsext.x	$$⊢\phi \to \forall x\in C\neg x\in N\left(C\setminus \left\{x\right\}\right)$$
	lbsext.s	$$⊢S=\left\{z\in 𝒫V|\left(C\subseteq z\wedge \forall x\in z\neg x\in N\left(z\setminus \left\{x\right\}\right)\right)\right\}$$
Assertion	lbsextlem1	$$⊢\phi \to S\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		lbsext.v	$$⊢V={\mathrm{Base}}_W$$
2		lbsext.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
3		lbsext.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lbsext.w	$$⊢\phi \to W\in \mathrm{LVec}$$
5		lbsext.c	$$⊢\phi \to C\subseteq V$$
6		lbsext.x	$$⊢\phi \to \forall x\in C\neg x\in N\left(C\setminus \left\{x\right\}\right)$$
7		lbsext.s	$$⊢S=\left\{z\in 𝒫V|\left(C\subseteq z\wedge \forall x\in z\neg x\in N\left(z\setminus \left\{x\right\}\right)\right)\right\}$$
8	1	fvexi	$$⊢V\in \mathrm{V}$$
9	8	elpw2	$$⊢C\in 𝒫V\leftrightarrow C\subseteq V$$
10	5 9	sylibr	$$⊢\phi \to C\in 𝒫V$$
11		ssid	$$⊢C\subseteq C$$
12	6 11	jctil	$$⊢\phi \to \left(C\subseteq C\wedge \forall x\in C\neg x\in N\left(C\setminus \left\{x\right\}\right)\right)$$
13		sseq2	$$⊢z=C\to \left(C\subseteq z\leftrightarrow C\subseteq C\right)$$
14		difeq1	$$⊢z=C\to z\setminus \left\{x\right\}=C\setminus \left\{x\right\}$$
15	14	fveq2d	$$⊢z=C\to N\left(z\setminus \left\{x\right\}\right)=N\left(C\setminus \left\{x\right\}\right)$$
16	15	eleq2d	$$⊢z=C\to \left(x\in N\left(z\setminus \left\{x\right\}\right)\leftrightarrow x\in N\left(C\setminus \left\{x\right\}\right)\right)$$
17	16	notbid	$$⊢z=C\to \left(\neg x\in N\left(z\setminus \left\{x\right\}\right)\leftrightarrow \neg x\in N\left(C\setminus \left\{x\right\}\right)\right)$$
18	17	raleqbi1dv	$$⊢z=C\to \left(\forall x\in z\neg x\in N\left(z\setminus \left\{x\right\}\right)\leftrightarrow \forall x\in C\neg x\in N\left(C\setminus \left\{x\right\}\right)\right)$$
19	13 18	anbi12d	$$⊢z=C\to \left(\left(C\subseteq z\wedge \forall x\in z\neg x\in N\left(z\setminus \left\{x\right\}\right)\right)\leftrightarrow \left(C\subseteq C\wedge \forall x\in C\neg x\in N\left(C\setminus \left\{x\right\}\right)\right)\right)$$
20	19 7	elrab2	$$⊢C\in S\leftrightarrow \left(C\in 𝒫V\wedge \left(C\subseteq C\wedge \forall x\in C\neg x\in N\left(C\setminus \left\{x\right\}\right)\right)\right)$$
21	10 12 20	sylanbrc	$$⊢\phi \to C\in S$$
22	21	ne0d	$$⊢\phi \to S\ne \varnothing$$