Metamath Proof Explorer


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 S A span A

Proof

Step Hyp Ref Expression
1 shsspwh S 𝒫
2 sstr A S S 𝒫 A 𝒫
3 1 2 mpan2 A S A 𝒫
4 3 unissd A S A 𝒫
5 unipw 𝒫 =
6 4 5 sseqtrdi A S A
7 spanss2 A A span A
8 6 7 syl A S A span A