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

Theorem phplem2 7602
 Description: Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus one of its elements. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.)
Hypotheses
Ref Expression
phplem2.1
phplem2.2
Assertion
Ref Expression
phplem2

Proof of Theorem phplem2
StepHypRef Expression
1 snex 4642 . . . . . 6
2 phplem2.2 . . . . . . 7
3 phplem2.1 . . . . . . 7
42, 3f1osn 5787 . . . . . 6
5 f1oen3g 7436 . . . . . 6
61, 4, 5mp2an 672 . . . . 5
7 difss 3592 . . . . . . 7
83, 7ssexi 4546 . . . . . 6
98enref 7453 . . . . 5
106, 9pm3.2i 455 . . . 4
11 incom 3652 . . . . . 6
12 ssrin 3684 . . . . . . . . 9
137, 12ax-mp 5 . . . . . . . 8
14 nnord 6595 . . . . . . . . 9
15 orddisj 4866 . . . . . . . . 9
1614, 15syl 16 . . . . . . . 8
1713, 16syl5sseq 3513 . . . . . . 7
18 ss0 3777 . . . . . . 7
1917, 18syl 16 . . . . . 6
2011, 19syl5eq 2507 . . . . 5
21 disjdif 3860 . . . . 5
2220, 21jctil 537 . . . 4
23 unen 7503 . . . 4
2410, 22, 23sylancr 663 . . 3