Theorem shsupunss

Description: The union of a set of subspaces is smaller than its supremum. (Contributed by NM, 26-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	shsupunss	$$⊢A\subseteq {\mathbf{S}}_{\mathscr{H}}\to \bigcup A\subseteq \mathrm{span}\left(\bigcup A\right)$$

Proof

Step	Hyp	Ref	Expression
1		shsspwh	$$⊢{\mathbf{S}}_{\mathscr{H}}\subseteq 𝒫\mathscr{H}$$
2		sstr	$$⊢\left(A\subseteq {\mathbf{S}}_{\mathscr{H}}\wedge {\mathbf{S}}_{\mathscr{H}}\subseteq 𝒫\mathscr{H}\right)\to A\subseteq 𝒫\mathscr{H}$$
3	1 2	mpan2	$$⊢A\subseteq {\mathbf{S}}_{\mathscr{H}}\to A\subseteq 𝒫\mathscr{H}$$
4	3	unissd	$$⊢A\subseteq {\mathbf{S}}_{\mathscr{H}}\to \bigcup A\subseteq \bigcup 𝒫\mathscr{H}$$
5		unipw	$$⊢\bigcup 𝒫\mathscr{H}=\mathscr{H}$$
6	4 5	sseqtrdi	$$⊢A\subseteq {\mathbf{S}}_{\mathscr{H}}\to \bigcup A\subseteq \mathscr{H}$$
7		spanss2	$$⊢\bigcup A\subseteq \mathscr{H}\to \bigcup A\subseteq \mathrm{span}\left(\bigcup A\right)$$
8	6 7	syl	$$⊢A\subseteq {\mathbf{S}}_{\mathscr{H}}\to \bigcup A\subseteq \mathrm{span}\left(\bigcup A\right)$$