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_ CH -> U. A C_ ( \/H ` A ) )

Proof

Step Hyp Ref Expression
1 chsspwh
 |-  CH C_ ~P ~H
2 sstr
 |-  ( ( A C_ CH /\ CH C_ ~P ~H ) -> A C_ ~P ~H )
3 1 2 mpan2
 |-  ( A C_ CH -> A C_ ~P ~H )
4 hsupunss
 |-  ( A C_ ~P ~H -> U. A C_ ( \/H ` A ) )
5 3 4 syl
 |-  ( A C_ CH -> U. A C_ ( \/H ` A ) )