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	⊢ ( 𝐴 ⊆ Sℋ → ∪ 𝐴 ⊆ ( span ‘ ∪ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		shsspwh	⊢ Sℋ ⊆ 𝒫 ℋ
2		sstr	⊢ ( ( 𝐴 ⊆ Sℋ ∧ Sℋ ⊆ 𝒫 ℋ ) → 𝐴 ⊆ 𝒫 ℋ )
3	1 2	mpan2	⊢ ( 𝐴 ⊆ Sℋ → 𝐴 ⊆ 𝒫 ℋ )
4	3	unissd	⊢ ( 𝐴 ⊆ Sℋ → ∪ 𝐴 ⊆ ∪ 𝒫 ℋ )
5		unipw	⊢ ∪ 𝒫 ℋ = ℋ
6	4 5	sseqtrdi	⊢ ( 𝐴 ⊆ Sℋ → ∪ 𝐴 ⊆ ℋ )
7		spanss2	⊢ ( ∪ 𝐴 ⊆ ℋ → ∪ 𝐴 ⊆ ( span ‘ ∪ 𝐴 ) )
8	6 7	syl	⊢ ( 𝐴 ⊆ Sℋ → ∪ 𝐴 ⊆ ( span ‘ ∪ 𝐴 ) )