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	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ) → ∪ 𝑆 ⊆ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		uniss	⊢ ( 𝑆 ⊆ 𝐶 → ∪ 𝑆 ⊆ ∪ 𝐶 )
2	1	adantl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ) → ∪ 𝑆 ⊆ ∪ 𝐶 )
3		mreuni	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ 𝐶 = 𝑋 )
4	3	adantr	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ) → ∪ 𝐶 = 𝑋 )
5	2 4	sseqtrd	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝐶 ) → ∪ 𝑆 ⊆ 𝑋 )