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 9219

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 9216, phplem2 9217, nneneq 9218, and this final piece of the proof. (Contributed by NM, 29-May-1998.) Avoid ax-pow 5335. (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 4375	. . . . . 6
2	sspsstr 4083	. . . . . 6
3	1, 2	mpan 690	. . . . 5
4	0pss 4422	. . . . . 6
5	df-ne 2933	. . . . . 6
6	4, 5	bitri 275	. . . . 5
7	3, 6	sylib 218	. . . 4
8	nn0suc 7888	. . . . 5
9	8	orcanai 1004	. . . 4
10	7, 9	sylan2 593	. . 3
11	pssnel 4446	. . . . . . . 8
12	pssss 4073	. . . . . . . . . . . . . . . . . . 19
13	ssdif 4119	. . . . . . . . . . . . . . . . . . . 20
14	disjsn 4687	. . . . . . . . . . . . . . . . . . . . . 22
15	disj3 4429	. . . . . . . . . . . . . . . . . . . . . 22
16	14, 15	bitr3i 277	. . . . . . . . . . . . . . . . . . . . 21
17	sseq1 3984	. . . . . . . . . . . . . . . . . . . . 21
18	16, 17	sylbi 217	. . . . . . . . . . . . . . . . . . . 20
19	13, 18	imbitrrid 246	. . . . . . . . . . . . . . . . . . 19
20	12, 19	syl5 34	. . . . . . . . . . . . . . . . . 18
21	peano2 7884	. . . . . . . . . . . . . . . . . . 19
22	nnfi 9179	. . . . . . . . . . . . . . . . . . 19
23	diffi 9187	. . . . . . . . . . . . . . . . . . 19
24	ssdomfi 9208	. . . . . . . . . . . . . . . . . . 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 9179	. . . . . . . . . . . . . . 15
32	31	ad2antrl 728	. . . . . . . . . . . . . 14
33	simpl 482	. . . . . . . . . . . . . 14
34	simpr 484	. . . . . . . . . . . . . 14
35	phplem1 9216	. . . . . . . . . . . . . . . . 17
36	ensymfib 9196	. . . . . . . . . . . . . . . . . . 19
37	31, 36	syl 17	. . . . . . . . . . . . . . . . . 18
38	37	adantr 480	. . . . . . . . . . . . . . . . 17
39	35, 38	mpbid 232	. . . . . . . . . . . . . . . 16
40	endom 8991	. . . . . . . . . . . . . . . 16
41	39, 40	syl 17	. . . . . . . . . . . . . . 15
42	domtrfir 9206	. . . . . . . . . . . . . . 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 8991	. . . . . . . . . . . . . . 15
53	domtrfir 9206	. . . . . . . . . . . . . . 15
54	52, 53	syl3an2 1164	. . . . . . . . . . . . . 14
55	31, 54	syl3an1 1163	. . . . . . . . . . . . 13
56	sssucid 6433	. . . . . . . . . . . . . . . . 17
57	ssdomfi 9208	. . . . . . . . . . . . . . . . 17
58	22, 56, 57	mpisyl 21	. . . . . . . . . . . . . . . 16
59	21, 58	syl 17	. . . . . . . . . . . . . . 15
60	59	adantr 480	. . . . . . . . . . . . . 14
61	sbthfi 9211	. . . . . . . . . . . . . . 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 7876	. . . . . . . . . . . . 13
68	nnord 7867	. . . . . . . . . . . . 13
69	67, 68	sylbi 217	. . . . . . . . . . . 12
70	vex 3463	. . . . . . . . . . . . 13
71	70	sucid 6435	. . . . . . . . . . . 12
72	nordeq 6371	. . . . . . . . . . . 12
73	69, 71, 72	sylancl 586	. . . . . . . . . . 11
74	nneneq 9218	. . . . . . . . . . . . . 14
75	67, 74	sylanb 581	. . . . . . . . . . . . 13
76	75	anidms 566	. . . . . . . . . . . 12
77	76	necon3bbid 2969	. . . . . . . . . . 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 4066	. . . . . 6
85	breq1 5122	. . . . . . 7
86	85	notbid 318	. . . . . 6
87	84, 86	imbi12d 344	. . . . 5
88	83, 87	syl5ibrcom 247	. . . 4
89	88	rexlimiv 3134	. . 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 2108 wne 2932 wrex 3060 cdif 3923 cin 3925 wss 3926 wpss 3927 c0 4308 csn 4601 class class class wbr 5119 word 6351 csuc 6354 com 7859 cen 8954 cdom 8955 cfn 8957

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pr 5402 ax-un 7727

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 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6483 df-fun 6532 df-fn 6533 df-f 6534 df-f1 6535 df-fo 6536 df-f1o 6537 df-fv 6538 df-om 7860 df-1o 8478 df-en 8958 df-dom 8959 df-fin 8961

This theorem is referenced by: php2 9220 php2OLD 9230 php3OLD 9231 omssrncard 43511 rr-phpd 44180