Theorem bj-ismoored0

Description: Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021)

	Ref	Expression
Assertion	bj-ismoored0	|- ( A e. Moore_ -> U. A e. A )

Proof

Step	Hyp	Ref	Expression
1		bj-ismoore	|- ( A e. Moore_ <-> A. x e. ~P A ( U. A i^i |^| x ) e. A )
2		0elpw	|- (/) e. ~P A
3		rint0	|- ( x = (/) -> ( U. A i^i |^| x ) = U. A )
4	3	eleq1d	|- ( x = (/) -> ( ( U. A i^i |^| x ) e. A <-> U. A e. A ) )
5	4	rspcv	|- ( (/) e. ~P A -> ( A. x e. ~P A ( U. A i^i |^| x ) e. A -> U. A e. A ) )
6	2 5	ax-mp	|- ( A. x e. ~P A ( U. A i^i |^| x ) e. A -> U. A e. A )
7	1 6	sylbi	|- ( A e. Moore_ -> U. A e. A )