Theorem phpm 6841

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 6828 through phplem4 6831, nneneq 6833, 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 3249	. . . . . . . . 9 |- ( x e. ( A \ B ) -> x e. A )
3		ne0i 3420	. . . . . . . . 9 |- ( x e. A -> A =/= (/) )
4	2, 3	syl 14	. . . . . . . 8 |- ( x e. ( A \ B ) -> A =/= (/) )
5	4	neneqd 2361	. . . . . . 7 |- ( x e. ( A \ B ) -> -. A = (/) )
6	5	ad2antlr 486	. . . . . 6 |- ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ A = (/) ) -> -. A = (/) )
7	1, 6	pm2.21dd 615	. . . . 5 |- ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ A = (/) ) -> -. A ~~ B )
8		php5dom 6839	. . . . . . . . . 10 |- ( y e. om -> -. suc y ~<_ y )
9	8	ad2antlr 486	. . . . . . . . 9 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> -. suc y ~<_ y )
10		simplr 525	. . . . . . . . . 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 2733	. . . . . . . . . . . . . . . 16 |- y e. _V
13	12	sucex 4481	. . . . . . . . . . . . . . 15 |- suc y e. _V
14		difss 3253	. . . . . . . . . . . . . . 15 |- ( suc y \ { x } ) C_ suc y
15	13, 14	ssexi 4125	. . . . . . . . . . . . . 14 |- ( suc y \ { x } ) e. _V
16		eldifn 3250	. . . . . . . . . . . . . . . 16 |- ( x e. ( A \ B ) -> -. x e. B )
17	16	ad3antlr 490	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> -. x e. B )
18		simpllr 529	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) -> B C_ A )
19	18	adantr 274	. . . . . . . . . . . . . . . 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 3185	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> B C_ suc y )
22		ssdif 3262	. . . . . . . . . . . . . . . 16 |- ( B C_ suc y -> ( B \ { x } ) C_ ( suc y \ { x } ) )
23		disjsn 3643	. . . . . . . . . . . . . . . . . 18 |- ( ( B i^i { x } ) = (/) <-> -. x e. B )
24		disj3 3466	. . . . . . . . . . . . . . . . . 18 |- ( ( B i^i { x } ) = (/) <-> B = ( B \ { x } ) )
25	23, 24	bitr3i 185	. . . . . . . . . . . . . . . . 17 |- ( -. x e. B <-> B = ( B \ { x } ) )
26		sseq1 3170	. . . . . . . . . . . . . . . . 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 6754	. . . . . . . . . . . . . 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 525	. . . . . . . . . . . . . 14 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> y e. om )
33	2	ad3antlr 490	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> x e. A )
34	33, 20	eleqtrd 2249	. . . . . . . . . . . . . 14 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> x e. suc y )
35		phplem3g 6832	. . . . . . . . . . . . . . 15 |- ( ( y e. om /\ x e. suc y ) -> y ~~ ( suc y \ { x } ) )
36	35	ensymd 6759	. . . . . . . . . . . . . 14 |- ( ( y e. om /\ x e. suc y ) -> ( suc y \ { x } ) ~~ y )
37	32, 34, 36	syl2anc 409	. . . . . . . . . . . . 13 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> ( suc y \ { x } ) ~~ y )
38		domentr 6767	. . . . . . . . . . . . 13 |- ( ( B ~<_ ( suc y \ { x } ) /\ ( suc y \ { x } ) ~~ y ) -> B ~<_ y )
39	31, 37, 38	syl2anc 409	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) -> B ~<_ y )
40	39	adantr 274	. . . . . . . . . . 11 |- ( ( ( ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) /\ y e. om ) /\ A = suc y ) /\ A ~~ B ) -> B ~<_ y )
41		endomtr 6766	. . . . . . . . . . 11 |- ( ( A ~~ B /\ B ~<_ y ) -> A ~<_ y )
42	11, 40, 41	syl2anc 409	. . . . . . . . . 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 4011	. . . . . . . . 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 660	. . . . . . . 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 2587	. . . . . 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 4586	. . . . . 6 |- ( A e. om -> ( A = (/) \/ E. y e. om A = suc y ) )
49	48	ad2antrr 485	. . . . 5 |- ( ( ( A e. om /\ B C_ A ) /\ x e. ( A \ B ) ) -> ( A = (/) \/ E. y e. om A = suc y ) )
50	7, 47, 49	mpjaodan 793	. . . 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 1812	. 2 |- ( ( A e. om /\ B C_ A ) -> ( E. x x e. ( A \ B ) -> -. A ~~ B ) )
53	52	3impia 1195	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 703   /\ w3a 973   = wceq 1348   E.wex 1485   e. wcel 2141   =/= wne 2340   E.wrex 2449   _Vcvv 2730   \ cdif 3118   i^i cin 3120   C_ wss 3121   (/)c0 3414   {csn 3581   class class class wbr 3987   suc csuc 4348   omcom 4572   ~~ cen 6714   ~<_ cdom 6715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-iinf 4570

This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-br 3988  df-opab 4049  df-tr 4086  df-id 4276  df-iord 4349  df-on 4351  df-suc 4354  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-er 6511  df-en 6717  df-dom 6718

This theorem is referenced by:  phpelm  6842