Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ismred2 Structured version   Unicode version

Theorem ismred2 13820
 Description: Properties that determine a Moore collection, using restricted intersection. (Contributed by Stefan O'Rear, 3-Apr-2015.)
Hypotheses
Ref Expression
ismred2.ss
ismred2.in
Assertion
Ref Expression
ismred2 Moore
Distinct variable groups:   ,   ,   ,

Proof of Theorem ismred2
StepHypRef Expression
1 ismred2.ss . 2
2 eqid 2435 . . . 4
3 rint0 4082 . . . 4
42, 3ax-mp 8 . . 3
5 0ss 3648 . . . 4
6 0ex 4331 . . . . 5
7 sseq1 3361 . . . . . . 7
87anbi2d 685 . . . . . 6
9 inteq 4045 . . . . . . . 8
109ineq2d 3534 . . . . . . 7
1110eleq1d 2501 . . . . . 6
128, 11imbi12d 312 . . . . 5
13 ismred2.in . . . . 5
146, 12, 13vtocl 2998 . . . 4
155, 14mpan2 653 . . 3
164, 15syl5eqelr 2520 . 2
17 simp2 958 . . . . 5
1813ad2ant1 978 . . . . 5
1917, 18sstrd 3350 . . . 4
20 simp3 959 . . . 4
21 rintn0 4173 . . . 4
2219, 20, 21syl2anc 643 . . 3