php - Metamath Proof Explorer

MPE Home Metamath Proof Explorer < Previous Next >
Nearby theorems

Mirrors > Home > MPE Home > Th. List > php Structured version Visualization version Unicode version

Theorem php 9183

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 put n + 1 pigeons into n holes (if each hole holds only one pigeon). The proof consists of phplem1 9180, phplem2 9181, nneneq 9182, and this final piece of the proof. (Contributed by NM, 29-May-1998.) Avoid ax-pow 5328. (Revised by BTernaryTau, 18-Nov-2024.)

**Assertion**
Ref	Expression
php

Proof of Theorem php

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1	0ss 4371	. . . . . 6
2	sspsstr 4079	. . . . . 6
3	1, 2	mpan 690	. . . . 5
4	0pss 4418	. . . . . 6
5	df-ne 2928	. . . . . 6
6	4, 5	bitri 275	. . . . 5
7	3, 6	sylib 218	. . . 4
8	nn0suc 7878	. . . . 5
9	8	orcanai 1004	. . . 4
10	7, 9	sylan2 593	. . 3
11	pssnel 4442	. . . . . . . 8
12	pssss 4069	. . . . . . . . . . . . . . . . . . 19
13	ssdif 4115	. . . . . . . . . . . . . . . . . . . 20
14	disjsn 4683	. . . . . . . . . . . . . . . . . . . . . 22
15	disj3 4425	. . . . . . . . . . . . . . . . . . . . . 22
16	14, 15	bitr3i 277	. . . . . . . . . . . . . . . . . . . . 21
17	sseq1 3980	. . . . . . . . . . . . . . . . . . . . 21
18	16, 17	sylbi 217	. . . . . . . . . . . . . . . . . . . 20
19	13, 18	imbitrrid 246	. . . . . . . . . . . . . . . . . . 19
20	12, 19	syl5 34	. . . . . . . . . . . . . . . . . 18
21	peano2 7874	. . . . . . . . . . . . . . . . . . 19
22	nnfi 9143	. . . . . . . . . . . . . . . . . . 19
23	diffi 9151	. . . . . . . . . . . . . . . . . . 19
24	ssdomfi 9172	. . . . . . . . . . . . . . . . . . 19
25	21, 22, 23, 24	4syl 19	. . . . . . . . . . . . . . . . . 18
26	20, 25	sylan9 507	. . . . . . . . . . . . . . . . 17
27	26	3impia 1117	. . . . . . . . . . . . . . . 16
28	27	3com23 1126	. . . . . . . . . . . . . . 15
29	28	3expa 1118	. . . . . . . . . . . . . 14
30	29	adantrr 717	. . . . . . . . . . . . 13
31	nnfi 9143	. . . . . . . . . . . . . . 15
32	31	ad2antrl 728	. . . . . . . . . . . . . 14
33	simpl 482	. . . . . . . . . . . . . 14
34	simpr 484	. . . . . . . . . . . . . 14
35	phplem1 9180	. . . . . . . . . . . . . . . . 17
36	ensymfib 9160	. . . . . . . . . . . . . . . . . . 19
37	31, 36	syl 17	. . . . . . . . . . . . . . . . . 18
38	37	adantr 480	. . . . . . . . . . . . . . . . 17
39	35, 38	mpbid 232	. . . . . . . . . . . . . . . 16
40	endom 8955	. . . . . . . . . . . . . . . 16
41	39, 40	syl 17	. . . . . . . . . . . . . . 15
42	domtrfir 9170	. . . . . . . . . . . . . . 15
43	41, 42	syl3an3 1165	. . . . . . . . . . . . . 14
44	32, 33, 34, 43	syl3anc 1373	. . . . . . . . . . . . 13
45	30, 44	sylancom 588	. . . . . . . . . . . 12
46	45	exp43 436	. . . . . . . . . . 11
47	46	com4r 94	. . . . . . . . . 10
48	47	imp 406	. . . . . . . . 9
49	48	exlimiv 1930	. . . . . . . 8
50	11, 49	mpcom 38	. . . . . . 7
51	simp1 1136	. . . . . . . . . . . . 13
52	endom 8955	. . . . . . . . . . . . . . 15
53	domtrfir 9170	. . . . . . . . . . . . . . 15
54	52, 53	syl3an2 1164	. . . . . . . . . . . . . 14
55	31, 54	syl3an1 1163	. . . . . . . . . . . . 13
56	sssucid 6422	. . . . . . . . . . . . . . . . 17
57	ssdomfi 9172	. . . . . . . . . . . . . . . . 17
58	22, 56, 57	mpisyl 21	. . . . . . . . . . . . . . . 16
59	21, 58	syl 17	. . . . . . . . . . . . . . 15
60	59	adantr 480	. . . . . . . . . . . . . 14
61	sbthfi 9175	. . . . . . . . . . . . . . 15
62	31, 61	syl3an1 1163	. . . . . . . . . . . . . 14
63	60, 62	mpd3an3 1464	. . . . . . . . . . . . 13
64	51, 55, 63	syl2anc 584	. . . . . . . . . . . 12
65	64	3com23 1126	. . . . . . . . . . 11
66	65	3expia 1121	. . . . . . . . . 10
67	peano2b 7866	. . . . . . . . . . . . 13
68	nnord 7857	. . . . . . . . . . . . 13
69	67, 68	sylbi 217	. . . . . . . . . . . 12
70	vex 3459	. . . . . . . . . . . . 13
71	70	sucid 6424	. . . . . . . . . . . 12
72	nordeq 6359	. . . . . . . . . . . 12
73	69, 71, 72	sylancl 586	. . . . . . . . . . 11
74	nneneq 9182	. . . . . . . . . . . . . 14
75	67, 74	sylanb 581	. . . . . . . . . . . . 13
76	75	anidms 566	. . . . . . . . . . . 12
77	76	necon3bbid 2964	. . . . . . . . . . 11
78	73, 77	mpbird 257	. . . . . . . . . 10
79	66, 78	nsyli 157	. . . . . . . . 9
80	79	expcom 413	. . . . . . . 8
81	80	pm2.43d 53	. . . . . . 7
82	50, 81	syli 39	. . . . . 6
83	82	com12 32	. . . . 5
84	psseq2 4062	. . . . . 6
85	breq1 5118	. . . . . . 7
86	85	notbid 318	. . . . . 6
87	84, 86	imbi12d 344	. . . . 5
88	83, 87	syl5ibrcom 247	. . . 4
89	88	rexlimiv 3129	. . 3
90	10, 89	syl 17	. 2
91	90	syldbl2 841	1

Colors of variables: wff setvar class

Syntax hints: wn 3 wi 4 wb 206 wa 395 w3a 1086 wceq 1540 wex 1779 wcel 2109 wne 2927 wrex 3055 cdif 3919 cin 3921 wss 3922 wpss 3923 c0 4304 csn 4597 class class class wbr 5115 word 6339 csuc 6342 com 7849 cen 8918 cdom 8919 cfn 8921

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5259 ax-nul 5269 ax-pr 5395 ax-un 7717

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2880 df-ne 2928 df-ral 3047 df-rex 3056 df-reu 3358 df-rab 3412 df-v 3457 df-sbc 3762 df-csb 3871 df-dif 3925 df-un 3927 df-in 3929 df-ss 3939 df-pss 3942 df-nul 4305 df-if 4497 df-pw 4573 df-sn 4598 df-pr 4600 df-op 4604 df-uni 4880 df-br 5116 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5541 df-eprel 5546 df-po 5554 df-so 5555 df-fr 5599 df-we 5601 df-xp 5652 df-rel 5653 df-cnv 5654 df-co 5655 df-dm 5656 df-rn 5657 df-res 5658 df-ima 5659 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6472 df-fun 6521 df-fn 6522 df-f 6523 df-f1 6524 df-fo 6525 df-f1o 6526 df-fv 6527 df-om 7850 df-1o 8442 df-en 8922 df-dom 8923 df-fin 8925

This theorem is referenced by: php2 9184 php3OLD 9190 omssrncard 43501 rr-phpd 44170