Theorem php3 7722

Description: Corollary of Pigeonhole Principle. If A is finite and B is a proper subset of A, the B is strictly less numerous than A. Stronger version of Corollary 6C of [Enderton] p. 135. (Contributed by NM, 22-Aug-2008.)

Assertion

Ref	Expression
php3	|- ( ( A e. Fin /\ B C. A ) -> B ~< A )

Proof of Theorem php3

Dummy variables x f y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfi 7558	. . 3 |- ( A e. Fin <-> E. x e. om A ~~ x )
2		relen 7540	. . . . . . . . 9 |- Rel ~~
3	2	brrelexi 5049	. . . . . . . 8 |- ( A ~~ x -> A e. _V )
4		pssss 3595	. . . . . . . 8 |- ( B C. A -> B C_ A )
5		ssdomg 7580	. . . . . . . . 9 |- ( A e. _V -> ( B C_ A -> B ~<_ A ) )
6	5	imp 429	. . . . . . . 8 |- ( ( A e. _V /\ B C_ A ) -> B ~<_ A )
7	3, 4, 6	syl2an 477	. . . . . . 7 |- ( ( A ~~ x /\ B C. A ) -> B ~<_ A )
8	7	adantll 713	. . . . . 6 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> B ~<_ A )
9		bren 7544	. . . . . . . . 9 |- ( A ~~ x <-> E. f f : A -1-1-onto-> x )
10		imass2 5382	. . . . . . . . . . . . . . . . 17 |- ( B C_ A -> ( f " B ) C_ ( f " A ) )
11	4, 10	syl 16	. . . . . . . . . . . . . . . 16 |- ( B C. A -> ( f " B ) C_ ( f " A ) )
12	11	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C_ ( f " A ) )
13		pssnel 3896	. . . . . . . . . . . . . . . . 17 |- ( B C. A -> E. y ( y e. A /\ -. y e. B ) )
14		eldif 3481	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( A \ B ) <-> ( y e. A /\ -. y e. B ) )
15		f1ofn 5823	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( f : A -1-1-onto-> x -> f Fn A )
16		difss 3627	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A \ B ) C_ A
17		fnfvima 6151	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f Fn A /\ ( A \ B ) C_ A /\ y e. ( A \ B ) ) -> ( f ` y ) e. ( f " ( A \ B ) ) )
18	17	3expia 1198	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( f Fn A /\ ( A \ B ) C_ A ) -> ( y e. ( A \ B ) -> ( f ` y ) e. ( f " ( A \ B ) ) ) )
19	15, 16, 18	sylancl 662	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> ( f ` y ) e. ( f " ( A \ B ) ) ) )
20		dff1o3 5828	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : A -1-1-onto-> x <-> ( f : A -onto-> x /\ Fun `' f ) )
21	20	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f : A -1-1-onto-> x -> Fun `' f )
22		imadif 5669	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( Fun `' f -> ( f " ( A \ B ) ) = ( ( f " A ) \ ( f " B ) ) )
23	21, 22	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( f : A -1-1-onto-> x -> ( f " ( A \ B ) ) = ( ( f " A ) \ ( f " B ) ) )
24	23	eleq2d 2527	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f : A -1-1-onto-> x -> ( ( f ` y ) e. ( f " ( A \ B ) ) <-> ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) ) )
25	19, 24	sylibd 214	. . . . . . . . . . . . . . . . . . . . 21 |- ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) ) )
26		n0i 3798	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
27	25, 26	syl6 33	. . . . . . . . . . . . . . . . . . . 20 |- ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
28	14, 27	syl5bir 218	. . . . . . . . . . . . . . . . . . 19 |- ( f : A -1-1-onto-> x -> ( ( y e. A /\ -. y e. B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
29	28	exlimdv 1725	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> x -> ( E. y ( y e. A /\ -. y e. B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
30	29	imp 429	. . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-onto-> x /\ E. y ( y e. A /\ -. y e. B ) ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
31	13, 30	sylan2 474	. . . . . . . . . . . . . . . 16 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
32		ssdif0 3888	. . . . . . . . . . . . . . . 16 |- ( ( f " A ) C_ ( f " B ) <-> ( ( f " A ) \ ( f " B ) ) = (/) )
33	31, 32	sylnibr 305	. . . . . . . . . . . . . . 15 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> -. ( f " A ) C_ ( f " B ) )
34		dfpss3 3586	. . . . . . . . . . . . . . 15 |- ( ( f " B ) C. ( f " A ) <-> ( ( f " B ) C_ ( f " A ) /\ -. ( f " A ) C_ ( f " B ) ) )
35	12, 33, 34	sylanbrc 664	. . . . . . . . . . . . . 14 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C. ( f " A ) )
36		imadmrn 5357	. . . . . . . . . . . . . . . . 17 |- ( f " dom f ) = ran f
37		f1odm 5826	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> x -> dom f = A )
38	37	imaeq2d 5347	. . . . . . . . . . . . . . . . 17 |- ( f : A -1-1-onto-> x -> ( f " dom f ) = ( f " A ) )
39		f1ofo 5829	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> x -> f : A -onto-> x )
40		forn 5804	. . . . . . . . . . . . . . . . . 18 |- ( f : A -onto-> x -> ran f = x )
41	39, 40	syl 16	. . . . . . . . . . . . . . . . 17 |- ( f : A -1-1-onto-> x -> ran f = x )
42	36, 38, 41	3eqtr3a 2522	. . . . . . . . . . . . . . . 16 |- ( f : A -1-1-onto-> x -> ( f " A ) = x )
43	42	psseq2d 3593	. . . . . . . . . . . . . . 15 |- ( f : A -1-1-onto-> x -> ( ( f " B ) C. ( f " A ) <-> ( f " B ) C. x ) )
44	43	adantr 465	. . . . . . . . . . . . . 14 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( ( f " B ) C. ( f " A ) <-> ( f " B ) C. x ) )
45	35, 44	mpbid 210	. . . . . . . . . . . . 13 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C. x )
46		php 7720	. . . . . . . . . . . . 13 |- ( ( x e. om /\ ( f " B ) C. x ) -> -. x ~~ ( f " B ) )
47	45, 46	sylan2 474	. . . . . . . . . . . 12 |- ( ( x e. om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> -. x ~~ ( f " B ) )
48		f1of1 5821	. . . . . . . . . . . . . . . 16 |- ( f : A -1-1-onto-> x -> f : A -1-1-> x )
49		f1ores 5836	. . . . . . . . . . . . . . . 16 |- ( ( f : A -1-1-> x /\ B C_ A ) -> ( f |` B ) : B -1-1-onto-> ( f " B ) )
50	48, 4, 49	syl2an 477	. . . . . . . . . . . . . . 15 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f |` B ) : B -1-1-onto-> ( f " B ) )
51		vex 3112	. . . . . . . . . . . . . . . . . 18 |- f e. _V
52	51	resex 5327	. . . . . . . . . . . . . . . . 17 |- ( f |` B ) e. _V
53		f1oeq1 5813	. . . . . . . . . . . . . . . . 17 |- ( y = ( f |` B ) -> ( y : B -1-1-onto-> ( f " B ) <-> ( f |` B ) : B -1-1-onto-> ( f " B ) ) )
54	52, 53	spcev 3201	. . . . . . . . . . . . . . . 16 |- ( ( f |` B ) : B -1-1-onto-> ( f " B ) -> E. y y : B -1-1-onto-> ( f " B ) )
55		bren 7544	. . . . . . . . . . . . . . . 16 |- ( B ~~ ( f " B ) <-> E. y y : B -1-1-onto-> ( f " B ) )
56	54, 55	sylibr 212	. . . . . . . . . . . . . . 15 |- ( ( f |` B ) : B -1-1-onto-> ( f " B ) -> B ~~ ( f " B ) )
57	50, 56	syl 16	. . . . . . . . . . . . . 14 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> B ~~ ( f " B ) )
58		entr 7586	. . . . . . . . . . . . . . 15 |- ( ( x ~~ B /\ B ~~ ( f " B ) ) -> x ~~ ( f " B ) )
59	58	expcom 435	. . . . . . . . . . . . . 14 |- ( B ~~ ( f " B ) -> ( x ~~ B -> x ~~ ( f " B ) ) )
60	57, 59	syl 16	. . . . . . . . . . . . 13 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( x ~~ B -> x ~~ ( f " B ) ) )
61	60	adantl 466	. . . . . . . . . . . 12 |- ( ( x e. om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> ( x ~~ B -> x ~~ ( f " B ) ) )
62	47, 61	mtod 177	. . . . . . . . . . 11 |- ( ( x e. om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> -. x ~~ B )
63	62	exp32 605	. . . . . . . . . 10 |- ( x e. om -> ( f : A -1-1-onto-> x -> ( B C. A -> -. x ~~ B ) ) )
64	63	exlimdv 1725	. . . . . . . . 9 |- ( x e. om -> ( E. f f : A -1-1-onto-> x -> ( B C. A -> -. x ~~ B ) ) )
65	9, 64	syl5bi 217	. . . . . . . 8 |- ( x e. om -> ( A ~~ x -> ( B C. A -> -. x ~~ B ) ) )
66	65	imp31 432	. . . . . . 7 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> -. x ~~ B )
67		entr 7586	. . . . . . . . . 10 |- ( ( B ~~ A /\ A ~~ x ) -> B ~~ x )
68	67	ex 434	. . . . . . . . 9 |- ( B ~~ A -> ( A ~~ x -> B ~~ x ) )
69		ensym 7583	. . . . . . . . 9 |- ( B ~~ x -> x ~~ B )
70	68, 69	syl6com 35	. . . . . . . 8 |- ( A ~~ x -> ( B ~~ A -> x ~~ B ) )
71	70	ad2antlr 726	. . . . . . 7 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> ( B ~~ A -> x ~~ B ) )
72	66, 71	mtod 177	. . . . . 6 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> -. B ~~ A )
73		brsdom 7557	. . . . . 6 |- ( B ~< A <-> ( B ~<_ A /\ -. B ~~ A ) )
74	8, 72, 73	sylanbrc 664	. . . . 5 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> B ~< A )
75	74	exp31 604	. . . 4 |- ( x e. om -> ( A ~~ x -> ( B C. A -> B ~< A ) ) )
76	75	rexlimiv 2943	. . 3 |- ( E. x e. om A ~~ x -> ( B C. A -> B ~< A ) )
77	1, 76	sylbi 195	. 2 |- ( A e. Fin -> ( B C. A -> B ~< A ) )
78	77	imp 429	1 |- ( ( A e. Fin /\ B C. A ) -> B ~< A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1395   E.wex 1613   e. wcel 1819   E.wrex 2808   _Vcvv 3109   \ cdif 3468   C_ wss 3471   C. wpss 3472   (/)c0 3793   class class class wbr 4456   `'ccnv 5007   dom cdm 5008   ran crn 5009   |` cres 5010   "cima 5011   Fun wfun 5588   Fn wfn 5589   -1-1->wf1 5591   -onto->wfo 5592   -1-1-onto->wf1o 5593   ` cfv 5594   omcom 6699   ~~ cen 7532   ~<_ cdom 7533   ~< csdm 7534   Fincfn 7535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-om 6700  df-er 7329  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539

This theorem is referenced by:  pssinf  7749  f1finf1o  7765  findcard3  7781  fofinf1o  7819  ackbij1b  8636  fincssdom  8720  fin23lem25  8721  canthp1lem2  9048  pwfseqlem4  9057  uzindi  12094  symggen  16622  pgpssslw  16761  pgpfaclem2  17260  ppiltx  23577  finminlem  30341