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

Theorem unblem1 7828
 Description: Lemma for unbnn 7832. After removing the successor of an element from an unbounded set of natural numbers, the intersection of the result belongs to the original unbounded set. (Contributed by NM, 3-Dec-2003.)
Assertion
Ref Expression
unblem1
Distinct variable groups:   ,,   ,,

Proof of Theorem unblem1
StepHypRef Expression
1 omsson 6701 . . . . . 6
2 sstr 3442 . . . . . 6
31, 2mpan2 678 . . . . 5
43ssdifssd 3573 . . . 4
6 ssel 3428 . . . . . 6
7 peano2b 6713 . . . . . 6
86, 7syl6ib 230 . . . . 5
9 eleq1 2519 . . . . . . . 8
109rexbidv 2903 . . . . . . 7
1110rspccva 3151 . . . . . 6
12 ssel 3428 . . . . . . . . . . 11
13 nnord 6705 . . . . . . . . . . . 12
14 ordn2lp 5446 . . . . . . . . . . . . . 14
15 imnan 424 . . . . . . . . . . . . . 14
1614, 15sylibr 216 . . . . . . . . . . . . 13
1716con2d 119 . . . . . . . . . . . 12
1813, 17syl 17 . . . . . . . . . . 11
1912, 18syl6 34 . . . . . . . . . 10
2019imdistand 699 . . . . . . . . 9
21 eldif 3416 . . . . . . . . . 10
22 ne0i 3739 . . . . . . . . . 10
2321, 22sylbir 217 . . . . . . . . 9
2420, 23syl6 34 . . . . . . . 8
2524expd 438 . . . . . . 7
2625rexlimdv 2879 . . . . . 6
2711, 26syl5 33 . . . . 5
288, 27sylan2d 485 . . . 4
2928impl 626 . . 3
30 onint 6627 . . 3
315, 29, 30syl2anc 667 . 2