Metamath Proof Explorer

Theorem mreuniss

Description: The union of a collection of closed sets is a subset. (Contributed by Zhi Wang, 29-Sep-2024)

Ref Expression
Assertion mreuniss 
|- ( ( C e. ( Moore ` X ) /\ S C_ C ) -> U. S C_ X )

Proof

Step Hyp Ref Expression
1 uniss 
 |-  ( S C_ C -> U. S C_ U. C )
2 1 adantl 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C ) -> U. S C_ U. C )
3 mreuni 
 |-  ( C e. ( Moore ` X ) -> U. C = X )
4 3 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C ) -> U. C = X )
5 2 4 sseqtrd 
 |-  ( ( C e. ( Moore ` X ) /\ S C_ C ) -> U. S C_ X )