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 ) )