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	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge S\subseteq C\right)\to \bigcup S\subseteq X$$

Proof

Step	Hyp	Ref	Expression
1		uniss	$$⊢S\subseteq C\to \bigcup S\subseteq \bigcup C$$
2	1	adantl	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge S\subseteq C\right)\to \bigcup S\subseteq \bigcup C$$
3		mreuni	$$⊢C\in \mathrm{Moore}\left(X\right)\to \bigcup C=X$$
4	3	adantr	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge S\subseteq C\right)\to \bigcup C=X$$
5	2 4	sseqtrd	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge S\subseteq C\right)\to \bigcup S\subseteq X$$