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 C_ SH -> U. A C_ ( span ` U. A ) )

Proof

Step	Hyp	Ref	Expression
1		shsspwh	|- SH C_ ~P ~H
2		sstr	|- ( ( A C_ SH /\ SH C_ ~P ~H ) -> A C_ ~P ~H )
3	1 2	mpan2	|- ( A C_ SH -> A C_ ~P ~H )
4	3	unissd	|- ( A C_ SH -> U. A C_ U. ~P ~H )
5		unipw	|- U. ~P ~H = ~H
6	4 5	sseqtrdi	|- ( A C_ SH -> U. A C_ ~H )
7		spanss2	|- ( U. A C_ ~H -> U. A C_ ( span ` U. A ) )
8	6 7	syl	|- ( A C_ SH -> U. A C_ ( span ` U. A ) )