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 ω B A ¬ A B

Proof

Step Hyp Ref Expression
1 0ss B
2 sspsstr B B A A
3 1 2 mpan B A A
4 0pss A A
5 df-ne A ¬ A =
6 4 5 bitri A ¬ A =
7 3 6 sylib B A ¬ A =
8 nn0suc A ω A = x ω A = suc x
9 8 orcanai A ω ¬ A = x ω A = suc x
10 7 9 sylan2 A ω B A x ω A = suc x
11 pssnel B suc x y y suc x ¬ y B
12 pssss B suc x B suc x
13 ssdif B suc x B y suc x y
14 disjsn B y = ¬ y B
15 disj3 B y = B = B y
16 14 15 bitr3i ¬ y B B = B y
17 sseq1 B = B y B suc x y B y suc x y
18 16 17 sylbi ¬ y B B suc x y B y suc x y
19 13 18 imbitrrid ¬ y B B suc x B suc x y
20 12 19 syl5 ¬ y B B suc x B suc x y
21 peano2 x ω suc x ω
22 nnfi suc x ω suc x Fin
23 diffi suc x Fin suc x y Fin
24 ssdomfi suc x y Fin B suc x y B suc x y
25 21 22 23 24 4syl x ω B suc x y B suc x y
26 20 25 sylan9 ¬ y B x ω B suc x B suc x y
27 26 3impia ¬ y B x ω B suc x B suc x y
28 27 3com23 ¬ y B B suc x x ω B suc x y
29 28 3expa ¬ y B B suc x x ω B suc x y
30 29 adantrr ¬ y B B suc x x ω y suc x B suc x y
31 nnfi x ω x Fin
32 31 ad2antrl B suc x y x ω y suc x x Fin
33 simpl B suc x y x ω y suc x B suc x y
34 simpr B suc x y x ω y suc x x ω y suc x
35 phplem1 x ω y suc x x suc x y
36 ensymfib x Fin x suc x y suc x y x
37 31 36 syl x ω x suc x y suc x y x
38 37 adantr x ω y suc x x suc x y suc x y x
39 35 38 mpbid x ω y suc x suc x y x
40 endom suc x y x suc x y x
41 39 40 syl x ω y suc x suc x y x
42 domtrfir x Fin B suc x y suc x y x B x
43 41 42 syl3an3 x Fin B suc x y x ω y suc x B x
44 32 33 34 43 syl3anc B suc x y x ω y suc x B x
45 30 44 sylancom ¬ y B B suc x x ω y suc x B x
46 45 exp43 ¬ y B B suc x x ω y suc x B x
47 46 com4r y suc x ¬ y B B suc x x ω B x
48 47 imp y suc x ¬ y B B suc x x ω B x
49 48 exlimiv y y suc x ¬ y B B suc x x ω B x
50 11 49 mpcom B suc x x ω B x
51 simp1 x ω suc x B B x x ω
52 endom suc x B suc x B
53 domtrfir x Fin suc x B B x suc x x
54 52 53 syl3an2 x Fin suc x B B x suc x x
55 31 54 syl3an1 x ω suc x B B x suc x x
56 sssucid x suc x
57 ssdomfi suc x Fin x suc x x suc x
58 22 56 57 mpisyl suc x ω x suc x
59 21 58 syl x ω x suc x
60 59 adantr x ω suc x x x suc x
61 sbthfi x Fin suc x x x suc x suc x x
62 31 61 syl3an1 x ω suc x x x suc x suc x x
63 60 62 mpd3an3 x ω suc x x suc x x
64 51 55 63 syl2anc x ω suc x B B x suc x x
65 64 3com23 x ω B x suc x B suc x x
66 65 3expia x ω B x suc x B suc x x
67 peano2b x ω suc x ω
68 nnord suc x ω Ord suc x
69 67 68 sylbi x ω Ord suc x
70 vex x V
71 70 sucid x suc x
72 nordeq Ord suc x x suc x suc x x
73 69 71 72 sylancl x ω suc x x
74 nneneq suc x ω x ω suc x x suc x = x
75 67 74 sylanb x ω x ω suc x x suc x = x
76 75 anidms x ω suc x x suc x = x
77 76 necon3bbid x ω ¬ suc x x suc x x
78 73 77 mpbird x ω ¬ suc x x
79 66 78 nsyli x ω B x x ω ¬ suc x B
80 79 expcom B x x ω x ω ¬ suc x B
81 80 pm2.43d B x x ω ¬ suc x B
82 50 81 syli B suc x x ω ¬ suc x B
83 82 com12 x ω B suc x ¬ suc x B
84 psseq2 A = suc x B A B suc x
85 breq1 A = suc x A B suc x B
86 85 notbid A = suc x ¬ A B ¬ suc x B
87 84 86 imbi12d A = suc x B A ¬ A B B suc x ¬ suc x B
88 83 87 syl5ibrcom x ω A = suc x B A ¬ A B
89 88 rexlimiv x ω A = suc x B A ¬ A B
90 10 89 syl A ω B A B A ¬ A B
91 90 syldbl2 A ω B A ¬ A B