Theorem php 5417

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 lemmas phplem1 5412 through phplem4 5415, nneneq 5416, and this final piece of the proof.

Assertion

Ref	Expression
php	|- ((A e. om /\ B C. A) -> -. A ~~ B)

Proof of Theorem php

Step	Hyp	Ref	Expression
1		nn0suc 3787	. . . . . . 7 |- (A e. om -> (A = (/) \/ E.x e. om A = suc x))
2	1	orcanai 751	. . . . . 6 |- ((A e. om /\ -. A = (/)) -> E.x e. om A = suc x)
3		0ss 2725	. . . . . . . 8 |- (/) C_ B
4		sspsstr 2547	. . . . . . . 8 |- (((/) C_ B /\ B C. A) -> (/) C. A)
5	3, 4	mpan 756	. . . . . . 7 |- (B C. A -> (/) C. A)
6		0pss 2734	. . . . . . . 8 |- ((/) C. A <-> A =/= (/))
7		df-ne 1856	. . . . . . . 8 |- (A =/= (/) <-> -. A = (/))
8	6, 7	bitri 189	. . . . . . 7 |- ((/) C. A <-> -. A = (/))
9	5, 8	sylib 214	. . . . . 6 |- (B C. A -> -. A = (/))
10	2, 9	sylan2 498	. . . . 5 |- ((A e. om /\ B C. A) -> E.x e. om A = suc x)
11		psseq2 2530	. . . . . . . 8 |- (A = suc x -> (B C. A <-> B C. suc x))
12		breq1 3161	. . . . . . . . 9 |- (A = suc x -> (A ~~ B <-> suc x ~~ B))
13	12	notbid 670	. . . . . . . 8 |- (A = suc x -> (-. A ~~ B <-> -. suc x ~~ B))
14	11, 13	imbi12d 685	. . . . . . 7 |- (A = suc x -> ((B C. A -> -. A ~~ B) <-> (B C. suc x -> -. suc x ~~ B)))
15		pssnel 2762	. . . . . . . . . 10 |- (B C. suc x -> E.y(y e. suc x /\ -. y e. B))
16		domentr 5291	. . . . . . . . . . . . . . 15 |- ((B ~<_ (suc x \ {y}) /\ (suc x \ {y}) ~~ x) -> B ~<_ x)
17		disjsn 2911	. . . . . . . . . . . . . . . . . . . . 21 |- ((B i^i {y}) = (/) <-> -. y e. B)
18		disj3 2742	. . . . . . . . . . . . . . . . . . . . 21 |- ((B i^i {y}) = (/) <-> B = (B \ {y}))
19	17, 18	bitr3i 191	. . . . . . . . . . . . . . . . . . . 20 |- (-. y e. B <-> B = (B \ {y}))
20		sseq1 2470	. . . . . . . . . . . . . . . . . . . 20 |- (B = (B \ {y}) -> (B C_ (suc x \ {y}) <-> (B \ {y}) C_ (suc x \ {y})))
21	19, 20	sylbi 215	. . . . . . . . . . . . . . . . . . 19 |- (-. y e. B -> (B C_ (suc x \ {y}) <-> (B \ {y}) C_ (suc x \ {y})))
22		ssdif 2572	. . . . . . . . . . . . . . . . . . 19 |- (B C_ suc x -> (B \ {y}) C_ (suc x \ {y}))
23	21, 22	syl5bir 226	. . . . . . . . . . . . . . . . . 18 |- (-. y e. B -> (B C_ suc x -> B C_ (suc x \ {y})))
24		visset 2128	. . . . . . . . . . . . . . . . . . . . 21 |- x e. _V
25	24	sucex 3703	. . . . . . . . . . . . . . . . . . . 20 |- suc x e. _V
26		difss 2567	. . . . . . . . . . . . . . . . . . . 20 |- (suc x \ {y}) C_ suc x
27	25, 26	ssexi 3271	. . . . . . . . . . . . . . . . . . 19 |- (suc x \ {y}) e. _V
28		ssdom2g 5279	. . . . . . . . . . . . . . . . . . 19 |- ((suc x \ {y}) e. _V -> (B C_ (suc x \ {y}) -> B ~<_ (suc x \ {y})))
29	27, 28	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- (B C_ (suc x \ {y}) -> B ~<_ (suc x \ {y}))
30	23, 29	syl6 25	. . . . . . . . . . . . . . . . 17 |- (-. y e. B -> (B C_ suc x -> B ~<_ (suc x \ {y})))
31		pssss 2537	. . . . . . . . . . . . . . . . 17 |- (B C. suc x -> B C_ suc x)
32	30, 31	syl5 20	. . . . . . . . . . . . . . . 16 |- (-. y e. B -> (B C. suc x -> B ~<_ (suc x \ {y})))
33	32	imp 375	. . . . . . . . . . . . . . 15 |- ((-. y e. B /\ B C. suc x) -> B ~<_ (suc x \ {y}))
34		visset 2128	. . . . . . . . . . . . . . . . 17 |- y e. _V
35	24, 34	phplem3 5414	. . . . . . . . . . . . . . . 16 |- ((x e. om /\ y e. suc x) -> x ~~ (suc x \ {y}))
36	27	ensym 5282	. . . . . . . . . . . . . . . 16 |- (x ~~ (suc x \ {y}) -> (suc x \ {y}) ~~ x)
37	35, 36	syl 12	. . . . . . . . . . . . . . 15 |- ((x e. om /\ y e. suc x) -> (suc x \ {y}) ~~ x)
38	16, 33, 37	syl2an 501	. . . . . . . . . . . . . 14 |- (((-. y e. B /\ B C. suc x) /\ (x e. om /\ y e. suc x)) -> B ~<_ x)
39	38	exp43 413	. . . . . . . . . . . . 13 |- (-. y e. B -> (B C. suc x -> (x e. om -> (y e. suc x -> B ~<_ x))))
40	39	com4r 45	. . . . . . . . . . . 12 |- (y e. suc x -> (-. y e. B -> (B C. suc x -> (x e. om -> B ~<_ x))))
41	40	imp 375	. . . . . . . . . . 11 |- ((y e. suc x /\ -. y e. B) -> (B C. suc x -> (x e. om -> B ~<_ x)))
42	41	19.23aiv 1512	. . . . . . . . . 10 |- (E.y(y e. suc x /\ -. y e. B) -> (B C. suc x -> (x e. om -> B ~<_ x)))
43	15, 42	mpcom 60	. . . . . . . . 9 |- (B C. suc x -> (x e. om -> B ~<_ x))
44		sbth 5331	. . . . . . . . . . . 12 |- ((suc x ~<_ x /\ x ~<_ suc x) -> suc x ~~ x)
45		endomtr 5290	. . . . . . . . . . . 12 |- ((suc x ~~ B /\ B ~<_ x) -> suc x ~<_ x)
46		sssucid 3557	. . . . . . . . . . . . 13 |- x C_ suc x
47		ssdom2g 5279	. . . . . . . . . . . . 13 |- (suc x e. _V -> (x C_ suc x -> x ~<_ suc x))
48	25, 46, 47	mp2 54	. . . . . . . . . . . 12 |- x ~<_ suc x
49	44, 45, 48	sylancl 522	. . . . . . . . . . 11 |- ((suc x ~~ B /\ B ~<_ x) -> suc x ~~ x)
50	49	expcom 401	. . . . . . . . . 10 |- (B ~<_ x -> (suc x ~~ B -> suc x ~~ x))
51		nordeq 3492	. . . . . . . . . . . 12 |- ((Ord suc x /\ x e. suc x) -> suc x =/= x)
52		peano2b 3779	. . . . . . . . . . . . 13 |- (x e. om <-> suc x e. om)
53		nnord 3770	. . . . . . . . . . . . 13 |- (suc x e. om -> Ord suc x)
54	52, 53	sylbi 215	. . . . . . . . . . . 12 |- (x e. om -> Ord suc x)
55	24	sucid 3558	. . . . . . . . . . . 12 |- x e. suc x
56	51, 54, 55	sylancl 522	. . . . . . . . . . 11 |- (x e. om -> suc x =/= x)
57		nneneq 5416	. . . . . . . . . . . . . 14 |- ((suc x e. om /\ x e. om) -> (suc x ~~ x <-> suc x = x))
58	57, 52	sylanb 496	. . . . . . . . . . . . 13 |- ((x e. om /\ x e. om) -> (suc x ~~ x <-> suc x = x))
59	58	anidms 478	. . . . . . . . . . . 12 |- (x e. om -> (suc x ~~ x <-> suc x = x))
60	59	necon3bbid 1869	. . . . . . . . . . 11 |- (x e. om -> (-. suc x ~~ x <-> suc x =/= x))
61	56, 60	mpbird 212	. . . . . . . . . 10 |- (x e. om -> -. suc x ~~ x)
62	50, 61	nsyli 135	. . . . . . . . 9 |- (B ~<_ x -> (x e. om -> -. suc x ~~ B))
63	43, 62	syli 65	. . . . . . . 8 |- (B C. suc x -> (x e. om -> -. suc x ~~ B))
64	63	com12 14	. . . . . . 7 |- (x e. om -> (B C. suc x -> -. suc x ~~ B))
65	14, 64	syl5cbir 227	. . . . . 6 |- (x e. om -> (A = suc x -> (B C. A -> -. A ~~ B)))
66	65	r19.23aiv 2045	. . . . 5 |- (E.x e. om A = suc x -> (B C. A -> -. A ~~ B))
67	10, 66	syl 12	. . . 4 |- ((A e. om /\ B C. A) -> (B C. A -> -. A ~~ B))
68	67	ex 400	. . 3 |- (A e. om -> (B C. A -> (B C. A -> -. A ~~ B)))
69	68	pm2.43d 79	. 2 |- (A e. om -> (B C. A -> -. A ~~ B))
70	69	imp 375	1 |- ((A e. om /\ B C. A) -> -. A ~~ B)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 162   /\ wa 239   = wceq 1136   e. wcel 1138  E.wex 1164   =/= wne 1854  E.wrex 1940  _Vcvv 2125   \ cdif 2423   i^i cin 2425   C_ wss 2426   C. wpss 2427  (/)c0 2701  {csn 2868   class class class wbr 3158  Ord word 3471  suc csuc 3474  omcom 3760   ~~ cen 5234   ~<_ cdom 5235

This theorem is referenced by:  php2 5418  php3 5419  top2usne 14618

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-rep 3243  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-rab 1946  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-if 2807  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-id 3401  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-lim 3477  df-suc 3478  df-om 3761  df-xp 3811  df-rel 3812  df-cnv 3813  df-co 3814  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fun 3819  df-fn 3820  df-f 3821  df-f1 3822  df-fo 3823  df-f1o 3824  df-fv 3825  df-er 5129  df-en 5238  df-dom 5239

Copyright terms: Public domain