Theorem ismred

Description: Properties that determine a Moore collection. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	ismred.ss	|- ( ph -> C C_ ~P X )
	ismred.ba	|- ( ph -> X e. C )
	ismred.in	|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> |^| s e. C )
Assertion	ismred	|- ( ph -> C e. ( Moore ` X ) )

Proof

Step	Hyp	Ref	Expression
1		ismred.ss	|- ( ph -> C C_ ~P X )
2		ismred.ba	|- ( ph -> X e. C )
3		ismred.in	|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> |^| s e. C )
4		velpw	|- ( s e. ~P C <-> s C_ C )
5	3	3expia	|- ( ( ph /\ s C_ C ) -> ( s =/= (/) -> |^| s e. C ) )
6	4 5	sylan2b	|- ( ( ph /\ s e. ~P C ) -> ( s =/= (/) -> |^| s e. C ) )
7	6	ralrimiva	|- ( ph -> A. s e. ~P C ( s =/= (/) -> |^| s e. C ) )
8		ismre	|- ( C e. ( Moore ` X ) <-> ( C C_ ~P X /\ X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) )
9	1 2 7 8	syl3anbrc	|- ( ph -> C e. ( Moore ` X ) )