This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )