This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in Moore (X) \land S \subseteq C) \to ⋃ S \subseteq X$

Step	Hyp	Ref	Expression
1		uniss	$⊢ S \subseteq C \to ⋃ S \subseteq ⋃ C$
2	1	adantl	$⊢ (C \in Moore (X) \land S \subseteq C) \to ⋃ S \subseteq ⋃ C$
3		mreuni	$⊢ C \in Moore (X) \to ⋃ C = X$
4	3	adantr	$⊢ (C \in Moore (X) \land S \subseteq C) \to ⋃ C = X$
5	2 4	sseqtrd	$⊢ (C \in Moore (X) \land S \subseteq C) \to ⋃ S \subseteq X$