Theorem phpm 6637

Description: Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. By "proper subset" here we mean that there is an element which is in the natural number and not in the subset, or in symbols E. x x e. ( A \ B ) (which is stronger than not being equal in the absence of excluded middle). 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 6624 through phplem4 6627, nneneq 6629, and this final piece of the proof. (Contributed by NM, 29-May-1998.)

Assertion

Ref	Expression
phpm	|- ( ( A e. om /\ B C_ A /\ E. x x e. ( A \ B ) ) -> -. A ~~ B )

Distinct variable groups:   x, A   x, B

Proof of Theorem phpm

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 109	. . . . . 6 |- ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ A = (/) ) -> A = (/) )
2		eldifi 3125	. . . . . . . . 9 |- ( x e. ( A \ B ) -> x e. A )
3		ne0i 3295	. . . . . . . . 9 |- ( x e. A -> A =/= (/) )
4	2, 3	syl 14	. . . . . . . 8 |- ( x e. ( A \ B ) -> A =/= (/) )
5	4	neneqd 2277	. . . . . . 7 |- ( x e. ( A \ B ) -> -. A = (/) )
6	5	ad2antlr 474	. . . . . 6 |- ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ A = (/) ) -> -. A = (/) )
7	1, 6	pm2.21dd 586	. . . . 5 |- ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ A = (/) ) -> -. A ~~ B )
8		php5dom 6635	. . . . . . . . . 10 |- ( y e. om -> -. suc y ~<_ y )
9	8	ad2antlr 474	. . . . . . . . 9 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> -. suc y ~<_ y )
10		simplr 498	. . . . . . . . . 10 |- ( ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) /\ A ~~ B ) -> A = suc y )
11		simpr 109	. . . . . . . . . . 11 |- ( ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) /\ A ~~ B ) -> A ~~ B )
12		vex 2625	. . . . . . . . . . . . . . . 16 |- y e. _V
13	12	sucex 4331	. . . . . . . . . . . . . . 15 |- suc y e. _V
14		difss 3129	. . . . . . . . . . . . . . 15 |- ( suc y \ { x } ) C_ suc y
15	13, 14	ssexi 3985	. . . . . . . . . . . . . 14 |- ( suc y \ { x } ) e. _V
16		eldifn 3126	. . . . . . . . . . . . . . . 16 |- ( x e. ( A \ B ) -> -. x e. B )
17	16	ad3antlr 478	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> -. x e. B )
18		simpllr 502	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) -> B C_ A )
19	18	adantr 271	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> B C_ A )
20		simpr 109	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> A = suc y )
21	19, 20	sseqtrd 3065	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> B C_ suc y )
22		ssdif 3138	. . . . . . . . . . . . . . . 16 |- ( B C_ suc y -> ( B \ { x } ) C_ ( suc y \ { x } ) )
23		disjsn 3510	. . . . . . . . . . . . . . . . . 18 |- ( ( B i^i { x } ) = (/) <-> -. x e. B )
24		disj3 3341	. . . . . . . . . . . . . . . . . 18 |- ( ( B i^i { x } ) = (/) <-> B = ( B \ { x } ) )
25	23, 24	bitr3i 185	. . . . . . . . . . . . . . . . 17 |- ( -. x e. B <-> B = ( B \ { x } ) )
26		sseq1 3050	. . . . . . . . . . . . . . . . 17 |- ( B = ( B \ { x } ) -> ( B C_ ( suc y \ { x } ) <-> ( B \ { x } ) C_ ( suc y \ { x } ) ) )
27	25, 26	sylbi 120	. . . . . . . . . . . . . . . 16 |- ( -. x e. B -> ( B C_ ( suc y \ { x } ) <-> ( B \ { x } ) C_ ( suc y \ { x } ) ) )
28	22, 27	syl5ibr 155	. . . . . . . . . . . . . . 15 |- ( -. x e. B -> ( B C_ suc y -> B C_ ( suc y \ { x } ) ) )
29	17, 21, 28	sylc 62	. . . . . . . . . . . . . 14 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> B C_ ( suc y \ { x } ) )
30		ssdomg 6551	. . . . . . . . . . . . . 14 |- ( ( suc y \ { x } ) e. _V -> ( B C_ ( suc y \ { x } ) -> B ~<_ ( suc y \ { x } ) ) )
31	15, 29, 30	mpsyl 65	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> B ~<_ ( suc y \ { x } ) )
32		simplr 498	. . . . . . . . . . . . . 14 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> y e. om )
33	2	ad3antlr 478	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> x e. A )
34	33, 20	eleqtrd 2167	. . . . . . . . . . . . . 14 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> x e. suc y )
35		phplem3g 6628	. . . . . . . . . . . . . . 15 |- ( ( y e. om /\ x e. suc y ) -> y ~~ ( suc y \ { x } ) )
36	35	ensymd 6556	. . . . . . . . . . . . . 14 |- ( ( y e. om /\ x e. suc y ) -> ( suc y \ { x } ) ~~ y )
37	32, 34, 36	syl2anc 404	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> ( suc y \ { x } ) ~~ y )
38		domentr 6564	. . . . . . . . . . . . 13 |- ( ( B ~<_ ( suc y \ { x } ) /\ ( suc y \ { x } ) ~~ y ) -> B ~<_ y )
39	31, 37, 38	syl2anc 404	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> B ~<_ y )
40	39	adantr 271	. . . . . . . . . . 11 |- ( ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) /\ A ~~ B ) -> B ~<_ y )
41		endomtr 6563	. . . . . . . . . . 11 |- ( ( A ~~ B /\ B ~<_ y ) -> A ~<_ y )
42	11, 40, 41	syl2anc 404	. . . . . . . . . 10 |- ( ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) /\ A ~~ B ) -> A ~<_ y )
43	10, 42	eqbrtrrd 3875	. . . . . . . . 9 |- ( ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) /\ A ~~ B ) -> suc y ~<_ y )
44	9, 43	mtand 627	. . . . . . . 8 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> -. A ~~ B )
45	44	ex 114	. . . . . . 7 |- ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) -> ( A = suc y -> -. A ~~ B ) )
46	45	rexlimdva 2491	. . . . . 6 |- ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) -> ( E. y e. om A = suc y -> -. A ~~ B ) )
47	46	imp 123	. . . . 5 |- ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ E. y e. om A = suc y ) -> -. A ~~ B )
48		nn0suc 4434	. . . . . 6 |- ( A e. om -> ( A = (/) \/ E. y e. om A = suc y ) )
49	48	ad2antrr 473	. . . . 5 |- ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) -> ( A = (/) \/ E. y e. om A = suc y ) )
50	7, 47, 49	mpjaodan 748	. . . 4 |- ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) -> -. A ~~ B )
51	50	ex 114	. . 3 |- ( ( A e. om /\ B C_ A ) -> ( x e. ( A \ B ) -> -. A ~~ B ) )
52	51	exlimdv 1748	. 2 |- ( ( A e. om /\ B C_ A ) -> ( E. x x e. ( A \ B ) -> -. A ~~ B ) )
53	52	3impia 1141	1 |- ( ( A e. om /\ B C_ A /\ E. x x e. ( A \ B ) ) -> -. A ~~ B )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 665   /\ w3a 925   = wceq 1290   E.wex 1427   e. wcel 1439   =/= wne 2256   E.wrex 2361   _Vcvv 2622   \ cdif 2999   i^i cin 3001   C_ wss 3002   (/)c0 3289   {csn 3452   class class class wbr 3853   suc csuc 4203   omcom 4420   ~~ cen 6511   ~<_ cdom 6512

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-nul 3973  ax-pow 4017  ax-pr 4047  ax-un 4271  ax-setind 4368  ax-iinf 4418

This theorem depends on definitions:  df-bi 116  df-dc 782  df-3or 926  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-rab 2369  df-v 2624  df-sbc 2844  df-dif 3004  df-un 3006  df-in 3008  df-ss 3015  df-nul 3290  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-int 3697  df-br 3854  df-opab 3908  df-tr 3945  df-id 4131  df-iord 4204  df-on 4206  df-suc 4209  df-iom 4421  df-xp 4460  df-rel 4461  df-cnv 4462  df-co 4463  df-dm 4464  df-rn 4465  df-res 4466  df-ima 4467  df-iota 4995  df-fun 5032  df-fn 5033  df-f 5034  df-f1 5035  df-fo 5036  df-f1o 5037  df-fv 5038  df-er 6308  df-en 6514  df-dom 6515

This theorem is referenced by:  phpelm  6638