Theorem bj-ismoored

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

	Ref	Expression
Hypotheses	bj-ismoored.1	|- ( ph -> A e. Moore_ )
	bj-ismoored.2	|- ( ph -> B C_ A )
Assertion	bj-ismoored	|- ( ph -> ( U. A i^i |^| B ) e. A )

Proof

Step	Hyp	Ref	Expression
1		bj-ismoored.1	|- ( ph -> A e. Moore_ )
2		bj-ismoored.2	|- ( ph -> B C_ A )
3		inteq	|- ( x = B -> |^| x = |^| B )
4	3	ineq2d	|- ( x = B -> ( U. A i^i |^| x ) = ( U. A i^i |^| B ) )
5	4	eleq1d	|- ( x = B -> ( ( U. A i^i |^| x ) e. A <-> ( U. A i^i |^| B ) e. A ) )
6		bj-ismoore	|- ( A e. Moore_ <-> A. x e. ~P A ( U. A i^i |^| x ) e. A )
7	1 6	sylib	|- ( ph -> A. x e. ~P A ( U. A i^i |^| x ) e. A )
8	1 2	sselpwd	|- ( ph -> B e. ~P A )
9	5 7 8	rspcdva	|- ( ph -> ( U. A i^i |^| B ) e. A )