Metamath Proof Explorer


Theorem chsupunss

Description: The union of a set of closed subspaces is smaller than its supremum. (Contributed by NM, 14-Aug-2002) (New usage is discouraged.)

Ref Expression
Assertion chsupunss A C A A

Proof

Step Hyp Ref Expression
1 chsspwh C 𝒫
2 sstr A C C 𝒫 A 𝒫
3 1 2 mpan2 A C A 𝒫
4 hsupunss A 𝒫 A A
5 3 4 syl A C A A