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 CMooreXSCSX

Proof

Step Hyp Ref Expression
1 uniss SCSC
2 1 adantl CMooreXSCSC
3 mreuni CMooreXC=X
4 3 adantr CMooreXSCC=X
5 2 4 sseqtrd CMooreXSCSX