Theorem lssuni

Description: The union of all subspaces is the vector space. (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	lssss.v	$$⊢V={\mathrm{Base}}_W$$
	lssss.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lssuni.w	$$⊢\phi \to W\in \mathrm{LMod}$$
Assertion	lssuni	$$⊢\phi \to \bigcup S=V$$

Proof

Step	Hyp	Ref	Expression
1		lssss.v	$$⊢V={\mathrm{Base}}_W$$
2		lssss.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3		lssuni.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		rabid2	$$⊢S=\left\{x\in S|x\subseteq V\right\}\leftrightarrow \forall x\in Sx\subseteq V$$
5	1 2	lssss	$$⊢x\in S\to x\subseteq V$$
6	4 5	mprgbir	$$⊢S=\left\{x\in S|x\subseteq V\right\}$$
7	6	unieqi	$$⊢\bigcup S=\bigcup \left\{x\in S|x\subseteq V\right\}$$
8	1 2	lss1	$$⊢W\in \mathrm{LMod}\to V\in S$$
9		unimax	$$⊢V\in S\to \bigcup \left\{x\in S|x\subseteq V\right\}=V$$
10	3 8 9	3syl	$$⊢\phi \to \bigcup \left\{x\in S|x\subseteq V\right\}=V$$
11	7 10	syl5eq	$$⊢\phi \to \bigcup S=V$$