Theorem bj-ismoored2

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 )
	bj-ismoored2.3	|- ( ph -> B =/= (/) )
Assertion	bj-ismoored2	|- ( ph -> |^| 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		bj-ismoored2.3	|- ( ph -> B =/= (/) )
4		intssuni2	|- ( ( B C_ A /\ B =/= (/) ) -> |^| B C_ U. A )
5	2 3 4	syl2anc	|- ( ph -> |^| B C_ U. A )
6		sseqin2	|- ( |^| B C_ U. A <-> ( U. A i^i |^| B ) = |^| B )
7	5 6	sylib	|- ( ph -> ( U. A i^i |^| B ) = |^| B )
8	1 2	bj-ismoored	|- ( ph -> ( U. A i^i |^| B ) e. A )
9	7 8	eqeltrrd	|- ( ph -> |^| B e. A )