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 e. ( Moore ` X ) -> U. C = X )

Proof

Step	Hyp	Ref	Expression
1		mre1cl	|- ( C e. ( Moore ` X ) -> X e. C )
2		mresspw	|- ( C e. ( Moore ` X ) -> C C_ ~P X )
3		elpwuni	|- ( X e. C -> ( C C_ ~P X <-> U. C = X ) )
4	3	biimpa	|- ( ( X e. C /\ C C_ ~P X ) -> U. C = X )
5	1 2 4	syl2anc	|- ( C e. ( Moore ` X ) -> U. C = X )