Theorem ismred2

Description: Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ismred2.ss	|- ( ph -> C C_ ~P X )
2		ismred2.in	|- ( ( ph /\ s C_ C ) -> ( X i^i |^| s ) e. C )
3		eqid	|- (/) = (/)
4		rint0	|- ( (/) = (/) -> ( X i^i |^| (/) ) = X )
5	3 4	ax-mp	|- ( X i^i |^| (/) ) = X
6		0ss	|- (/) C_ C
7		0ex	|- (/) e. _V
8		sseq1	|- ( s = (/) -> ( s C_ C <-> (/) C_ C ) )
9	8	anbi2d	|- ( s = (/) -> ( ( ph /\ s C_ C ) <-> ( ph /\ (/) C_ C ) ) )
10		inteq	|- ( s = (/) -> |^| s = |^| (/) )
11	10	ineq2d	|- ( s = (/) -> ( X i^i |^| s ) = ( X i^i |^| (/) ) )
12	11	eleq1d	|- ( s = (/) -> ( ( X i^i |^| s ) e. C <-> ( X i^i |^| (/) ) e. C ) )
13	9 12	imbi12d	|- ( s = (/) -> ( ( ( ph /\ s C_ C ) -> ( X i^i |^| s ) e. C ) <-> ( ( ph /\ (/) C_ C ) -> ( X i^i |^| (/) ) e. C ) ) )
14	7 13 2	vtocl	|- ( ( ph /\ (/) C_ C ) -> ( X i^i |^| (/) ) e. C )
15	6 14	mpan2	|- ( ph -> ( X i^i |^| (/) ) e. C )
16	5 15	eqeltrrid	|- ( ph -> X e. C )
17		simp2	|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> s C_ C )
18	1	3ad2ant1	|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> C C_ ~P X )
19	17 18	sstrd	|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> s C_ ~P X )
20		simp3	|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> s =/= (/) )
21		rintn0	|- ( ( s C_ ~P X /\ s =/= (/) ) -> ( X i^i |^| s ) = |^| s )
22	19 20 21	syl2anc	|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> ( X i^i |^| s ) = |^| s )
23	2	3adant3	|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> ( X i^i |^| s ) e. C )
24	22 23	eqeltrrd	|- ( ( ph /\ s C_ C /\ s =/= (/) ) -> |^| s e. C )
25	1 16 24	ismred	|- ( ph -> C e. ( Moore ` X ) )