Description: Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers. (Contributed by NM, 28-May-1998) (Revised by Mario Carneiro, 24-Jun-2015) Avoid ax-pow . (Revised by BTernaryTau, 4-Nov-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | phplem2.1 | |
|
Assertion | phplem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | phplem2.1 | |
|
2 | bren | |
|
3 | f1of1 | |
|
4 | nnfi | |
|
5 | sssucid | |
|
6 | f1imaenfi | |
|
7 | 5 6 | mp3an2 | |
8 | 3 4 7 | syl2anr | |
9 | ensymfib | |
|
10 | 4 9 | syl | |
11 | 10 | adantr | |
12 | 8 11 | mpbird | |
13 | nnord | |
|
14 | orddif | |
|
15 | 13 14 | syl | |
16 | 15 | imaeq2d | |
17 | f1ofn | |
|
18 | 1 | sucid | |
19 | fnsnfv | |
|
20 | 17 18 19 | sylancl | |
21 | 20 | difeq2d | |
22 | imadmrn | |
|
23 | 22 | eqcomi | |
24 | f1ofo | |
|
25 | forn | |
|
26 | 24 25 | syl | |
27 | f1odm | |
|
28 | 27 | imaeq2d | |
29 | 23 26 28 | 3eqtr3a | |
30 | 29 | difeq1d | |
31 | dff1o3 | |
|
32 | imadif | |
|
33 | 31 32 | simplbiim | |
34 | 21 30 33 | 3eqtr4rd | |
35 | 16 34 | sylan9eq | |
36 | 12 35 | breqtrd | |
37 | fnfvelrn | |
|
38 | 17 18 37 | sylancl | |
39 | 25 | eleq2d | |
40 | 24 39 | syl | |
41 | 38 40 | mpbid | |
42 | phplem1 | |
|
43 | 41 42 | sylan2 | |
44 | nnfi | |
|
45 | ensymfib | |
|
46 | 44 45 | syl | |
47 | 46 | adantr | |
48 | 43 47 | mpbid | |
49 | entrfil | |
|
50 | 4 49 | syl3an1 | |
51 | 48 50 | syl3an3 | |
52 | 51 | 3expa | |
53 | 36 52 | syldanl | |
54 | 53 | anandirs | |
55 | 54 | ex | |
56 | 55 | exlimdv | |
57 | 2 56 | syl5bi | |