Theorem mreuni

Description: Since the entire base set of a Moore collection is the greatest element of it, the base set can be recovered from a Moore collection by set union. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Assertion	mreuni	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ 𝐶 = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		mre1cl	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 )
2		mresspw	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 ⊆ 𝒫 𝑋 )
3		elpwuni	⊢ ( 𝑋 ∈ 𝐶 → ( 𝐶 ⊆ 𝒫 𝑋 ↔ ∪ 𝐶 = 𝑋 ) )
4	3	biimpa	⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝐶 ⊆ 𝒫 𝑋 ) → ∪ 𝐶 = 𝑋 )
5	1 2 4	syl2anc	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ 𝐶 = 𝑋 )