Metamath Proof Explorer


Theorem php

Description: Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. Theorem (Pigeonhole Principle) of Enderton p. 134. The theorem is so-called because you can't putn + 1 pigeons inton holes (if each hole holds only one pigeon). The proof consists of phplem1 , phplem2 , nneneq , and this final piece of the proof. (Contributed by NM, 29-May-1998) Avoid ax-pow . (Revised by BTernaryTau, 18-Nov-2024)

Ref Expression
Assertion php AωBA¬AB

Proof

Step Hyp Ref Expression
1 0ss B
2 sspsstr BBAA
3 1 2 mpan BAA
4 0pss AA
5 df-ne A¬A=
6 4 5 bitri A¬A=
7 3 6 sylib BA¬A=
8 nn0suc AωA=xωA=sucx
9 8 orcanai Aω¬A=xωA=sucx
10 7 9 sylan2 AωBAxωA=sucx
11 pssnel Bsucxyysucx¬yB
12 pssss BsucxBsucx
13 ssdif BsucxBysucxy
14 disjsn By=¬yB
15 disj3 By=B=By
16 14 15 bitr3i ¬yBB=By
17 sseq1 B=ByBsucxyBysucxy
18 16 17 sylbi ¬yBBsucxyBysucxy
19 13 18 syl5ibr ¬yBBsucxBsucxy
20 12 19 syl5 ¬yBBsucxBsucxy
21 peano2 xωsucxω
22 nnfi sucxωsucxFin
23 diffi sucxFinsucxyFin
24 21 22 23 3syl xωsucxyFin
25 ssdomfi sucxyFinBsucxyBsucxy
26 24 25 syl xωBsucxyBsucxy
27 20 26 sylan9 ¬yBxωBsucxBsucxy
28 27 3impia ¬yBxωBsucxBsucxy
29 28 3com23 ¬yBBsucxxωBsucxy
30 29 3expa ¬yBBsucxxωBsucxy
31 30 adantrr ¬yBBsucxxωysucxBsucxy
32 nnfi xωxFin
33 32 ad2antrl BsucxyxωysucxxFin
34 simpl BsucxyxωysucxBsucxy
35 simpr Bsucxyxωysucxxωysucx
36 phplem1 xωysucxxsucxy
37 ensymfib xFinxsucxysucxyx
38 32 37 syl xωxsucxysucxyx
39 38 adantr xωysucxxsucxysucxyx
40 36 39 mpbid xωysucxsucxyx
41 endom sucxyxsucxyx
42 40 41 syl xωysucxsucxyx
43 domtrfir xFinBsucxysucxyxBx
44 42 43 syl3an3 xFinBsucxyxωysucxBx
45 33 34 35 44 syl3anc BsucxyxωysucxBx
46 31 45 sylancom ¬yBBsucxxωysucxBx
47 46 exp43 ¬yBBsucxxωysucxBx
48 47 com4r ysucx¬yBBsucxxωBx
49 48 imp ysucx¬yBBsucxxωBx
50 49 exlimiv yysucx¬yBBsucxxωBx
51 11 50 mpcom BsucxxωBx
52 simp1 xωsucxBBxxω
53 endom sucxBsucxB
54 domtrfir xFinsucxBBxsucxx
55 53 54 syl3an2 xFinsucxBBxsucxx
56 32 55 syl3an1 xωsucxBBxsucxx
57 sssucid xsucx
58 ssdomfi sucxFinxsucxxsucx
59 22 57 58 mpisyl sucxωxsucx
60 21 59 syl xωxsucx
61 60 adantr xωsucxxxsucx
62 sbthfi xFinsucxxxsucxsucxx
63 32 62 syl3an1 xωsucxxxsucxsucxx
64 61 63 mpd3an3 xωsucxxsucxx
65 52 56 64 syl2anc xωsucxBBxsucxx
66 65 3com23 xωBxsucxBsucxx
67 66 3expia xωBxsucxBsucxx
68 peano2b xωsucxω
69 nnord sucxωOrdsucx
70 68 69 sylbi xωOrdsucx
71 vex xV
72 71 sucid xsucx
73 nordeq Ordsucxxsucxsucxx
74 70 72 73 sylancl xωsucxx
75 nneneq sucxωxωsucxxsucx=x
76 68 75 sylanb xωxωsucxxsucx=x
77 76 anidms xωsucxxsucx=x
78 77 necon3bbid xω¬sucxxsucxx
79 74 78 mpbird xω¬sucxx
80 67 79 nsyli xωBxxω¬sucxB
81 80 expcom Bxxωxω¬sucxB
82 81 pm2.43d Bxxω¬sucxB
83 51 82 syli Bsucxxω¬sucxB
84 83 com12 xωBsucx¬sucxB
85 psseq2 A=sucxBABsucx
86 breq1 A=sucxABsucxB
87 86 notbid A=sucx¬AB¬sucxB
88 85 87 imbi12d A=sucxBA¬ABBsucx¬sucxB
89 84 88 syl5ibrcom xωA=sucxBA¬AB
90 89 rexlimiv xωA=sucxBA¬AB
91 10 90 syl AωBABA¬AB
92 91 syldbl2 AωBA¬AB