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

Proof

Step	Hyp	Ref	Expression
1		mre1cl	$$⊢C\in \mathrm{Moore}\left(X\right)\to X\in C$$
2		mresspw	$$⊢C\in \mathrm{Moore}\left(X\right)\to C\subseteq 𝒫X$$
3		elpwuni	$$⊢X\in C\to \left(C\subseteq 𝒫X\leftrightarrow \bigcup C=X\right)$$
4	3	biimpa	$$⊢\left(X\in C\wedge C\subseteq 𝒫X\right)\to \bigcup C=X$$
5	1 2 4	syl2anc	$$⊢C\in \mathrm{Moore}\left(X\right)\to \bigcup C=X$$