Theorem php3 7755

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 7590	. . 3 |- ( A e. Fin <-> E. x e. om A ~~ x )
2		relen 7571	. . . . . . . . 9 |- Rel ~~
3	2	brrelexi 4874	. . . . . . . 8 |- ( A ~~ x -> A e. _V )
4		pssss 3527	. . . . . . . 8 |- ( B C. A -> B C_ A )
5		ssdomg 7612	. . . . . . . . 9 |- ( A e. _V -> ( B C_ A -> B ~<_ A ) )
6	5	imp 431	. . . . . . . 8 |- ( ( A e. _V /\ B C_ A ) -> B ~<_ A )
7	3, 4, 6	syl2an 480	. . . . . . 7 |- ( ( A ~~ x /\ B C. A ) -> B ~<_ A )
8	7	adantll 719	. . . . . 6 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> B ~<_ A )
9		bren 7575	. . . . . . . . 9 |- ( A ~~ x <-> E. f f : A -1-1-onto-> x )
10		imass2 5203	. . . . . . . . . . . . . . . . 17 |- ( B C_ A -> ( f " B ) C_ ( f " A ) )
11	4, 10	syl 17	. . . . . . . . . . . . . . . 16 |- ( B C. A -> ( f " B ) C_ ( f " A ) )
12	11	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C_ ( f " A ) )
13		pssnel 3831	. . . . . . . . . . . . . . . . 17 |- ( B C. A -> E. y ( y e. A /\ -. y e. B ) )
14		eldif 3413	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( A \ B ) <-> ( y e. A /\ -. y e. B ) )
15		f1ofn 5813	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( f : A -1-1-onto-> x -> f Fn A )
16		difss 3559	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A \ B ) C_ A
17		fnfvima 6141	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f Fn A /\ ( A \ B ) C_ A /\ y e. ( A \ B ) ) -> ( f ` y ) e. ( f " ( A \ B ) ) )
18	17	3expia 1209	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( f Fn A /\ ( A \ B ) C_ A ) -> ( y e. ( A \ B ) -> ( f ` y ) e. ( f " ( A \ B ) ) ) )
19	15, 16, 18	sylancl 667	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> ( f ` y ) e. ( f " ( A \ B ) ) ) )
20		dff1o3 5818	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : A -1-1-onto-> x <-> ( f : A -onto-> x /\ Fun `' f ) )
21	20	simprbi 466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f : A -1-1-onto-> x -> Fun `' f )
22		imadif 5656	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( Fun `' f -> ( f " ( A \ B ) ) = ( ( f " A ) \ ( f " B ) ) )
23	21, 22	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( f : A -1-1-onto-> x -> ( f " ( A \ B ) ) = ( ( f " A ) \ ( f " B ) ) )
24	23	eleq2d 2513	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f : A -1-1-onto-> x -> ( ( f ` y ) e. ( f " ( A \ B ) ) <-> ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) ) )
25	19, 24	sylibd 218	. . . . . . . . . . . . . . . . . . . . 21 |- ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) ) )
26		n0i 3735	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
27	25, 26	syl6 34	. . . . . . . . . . . . . . . . . . . 20 |- ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
28	14, 27	syl5bir 222	. . . . . . . . . . . . . . . . . . 19 |- ( f : A -1-1-onto-> x -> ( ( y e. A /\ -. y e. B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
29	28	exlimdv 1778	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> x -> ( E. y ( y e. A /\ -. y e. B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
30	29	imp 431	. . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-onto-> x /\ E. y ( y e. A /\ -. y e. B ) ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
31	13, 30	sylan2 477	. . . . . . . . . . . . . . . 16 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
32		ssdif0 3822	. . . . . . . . . . . . . . . 16 |- ( ( f " A ) C_ ( f " B ) <-> ( ( f " A ) \ ( f " B ) ) = (/) )
33	31, 32	sylnibr 307	. . . . . . . . . . . . . . 15 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> -. ( f " A ) C_ ( f " B ) )
34		dfpss3 3518	. . . . . . . . . . . . . . 15 |- ( ( f " B ) C. ( f " A ) <-> ( ( f " B ) C_ ( f " A ) /\ -. ( f " A ) C_ ( f " B ) ) )
35	12, 33, 34	sylanbrc 669	. . . . . . . . . . . . . 14 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C. ( f " A ) )
36		imadmrn 5177	. . . . . . . . . . . . . . . . 17 |- ( f " dom f ) = ran f
37		f1odm 5816	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> x -> dom f = A )
38	37	imaeq2d 5167	. . . . . . . . . . . . . . . . 17 |- ( f : A -1-1-onto-> x -> ( f " dom f ) = ( f " A ) )
39		f1ofo 5819	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> x -> f : A -onto-> x )
40		forn 5794	. . . . . . . . . . . . . . . . . 18 |- ( f : A -onto-> x -> ran f = x )
41	39, 40	syl 17	. . . . . . . . . . . . . . . . 17 |- ( f : A -1-1-onto-> x -> ran f = x )
42	36, 38, 41	3eqtr3a 2508	. . . . . . . . . . . . . . . 16 |- ( f : A -1-1-onto-> x -> ( f " A ) = x )
43	42	psseq2d 3525	. . . . . . . . . . . . . . 15 |- ( f : A -1-1-onto-> x -> ( ( f " B ) C. ( f " A ) <-> ( f " B ) C. x ) )
44	43	adantr 467	. . . . . . . . . . . . . 14 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( ( f " B ) C. ( f " A ) <-> ( f " B ) C. x ) )
45	35, 44	mpbid 214	. . . . . . . . . . . . 13 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C. x )
46		php 7753	. . . . . . . . . . . . 13 |- ( ( x e. om /\ ( f " B ) C. x ) -> -. x ~~ ( f " B ) )
47	45, 46	sylan2 477	. . . . . . . . . . . 12 |- ( ( x e. om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> -. x ~~ ( f " B ) )
48		f1of1 5811	. . . . . . . . . . . . . . . 16 |- ( f : A -1-1-onto-> x -> f : A -1-1-> x )
49		f1ores 5826	. . . . . . . . . . . . . . . 16 |- ( ( f : A -1-1-> x /\ B C_ A ) -> ( f |` B ) : B -1-1-onto-> ( f " B ) )
50	48, 4, 49	syl2an 480	. . . . . . . . . . . . . . 15 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f |` B ) : B -1-1-onto-> ( f " B ) )
51		vex 3047	. . . . . . . . . . . . . . . . . 18 |- f e. _V
52	51	resex 5147	. . . . . . . . . . . . . . . . 17 |- ( f |` B ) e. _V
53		f1oeq1 5803	. . . . . . . . . . . . . . . . 17 |- ( y = ( f |` B ) -> ( y : B -1-1-onto-> ( f " B ) <-> ( f |` B ) : B -1-1-onto-> ( f " B ) ) )
54	52, 53	spcev 3140	. . . . . . . . . . . . . . . 16 |- ( ( f |` B ) : B -1-1-onto-> ( f " B ) -> E. y y : B -1-1-onto-> ( f " B ) )
55		bren 7575	. . . . . . . . . . . . . . . 16 |- ( B ~~ ( f " B ) <-> E. y y : B -1-1-onto-> ( f " B ) )
56	54, 55	sylibr 216	. . . . . . . . . . . . . . 15 |- ( ( f |` B ) : B -1-1-onto-> ( f " B ) -> B ~~ ( f " B ) )
57	50, 56	syl 17	. . . . . . . . . . . . . 14 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> B ~~ ( f " B ) )
58		entr 7618	. . . . . . . . . . . . . . 15 |- ( ( x ~~ B /\ B ~~ ( f " B ) ) -> x ~~ ( f " B ) )
59	58	expcom 437	. . . . . . . . . . . . . 14 |- ( B ~~ ( f " B ) -> ( x ~~ B -> x ~~ ( f " B ) ) )
60	57, 59	syl 17	. . . . . . . . . . . . 13 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( x ~~ B -> x ~~ ( f " B ) ) )
61	60	adantl 468	. . . . . . . . . . . 12 |- ( ( x e. om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> ( x ~~ B -> x ~~ ( f " B ) ) )
62	47, 61	mtod 181	. . . . . . . . . . 11 |- ( ( x e. om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> -. x ~~ B )
63	62	exp32 609	. . . . . . . . . 10 |- ( x e. om -> ( f : A -1-1-onto-> x -> ( B C. A -> -. x ~~ B ) ) )
64	63	exlimdv 1778	. . . . . . . . 9 |- ( x e. om -> ( E. f f : A -1-1-onto-> x -> ( B C. A -> -. x ~~ B ) ) )
65	9, 64	syl5bi 221	. . . . . . . 8 |- ( x e. om -> ( A ~~ x -> ( B C. A -> -. x ~~ B ) ) )
66	65	imp31 434	. . . . . . 7 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> -. x ~~ B )
67		entr 7618	. . . . . . . . . 10 |- ( ( B ~~ A /\ A ~~ x ) -> B ~~ x )
68	67	ex 436	. . . . . . . . 9 |- ( B ~~ A -> ( A ~~ x -> B ~~ x ) )
69		ensym 7615	. . . . . . . . 9 |- ( B ~~ x -> x ~~ B )
70	68, 69	syl6com 36	. . . . . . . 8 |- ( A ~~ x -> ( B ~~ A -> x ~~ B ) )
71	70	ad2antlr 732	. . . . . . 7 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> ( B ~~ A -> x ~~ B ) )
72	66, 71	mtod 181	. . . . . 6 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> -. B ~~ A )
73		brsdom 7589	. . . . . 6 |- ( B ~< A <-> ( B ~<_ A /\ -. B ~~ A ) )
74	8, 72, 73	sylanbrc 669	. . . . 5 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> B ~< A )
75	74	exp31 608	. . . 4 |- ( x e. om -> ( A ~~ x -> ( B C. A -> B ~< A ) ) )
76	75	rexlimiv 2872	. . 3 |- ( E. x e. om A ~~ x -> ( B C. A -> B ~< A ) )
77	1, 76	sylbi 199	. 2 |- ( A e. Fin -> ( B C. A -> B ~< A ) )
78	77	imp 431	1 |- ( ( A e. Fin /\ B C. A ) -> B ~< A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1443   E.wex 1662   e. wcel 1886   E.wrex 2737   _Vcvv 3044   \ cdif 3400   C_ wss 3403   C. wpss 3404   (/)c0 3730   class class class wbr 4401   `'ccnv 4832   dom cdm 4833   ran crn 4834   |` cres 4835   "cima 4836   Fun wfun 5575   Fn wfn 5576   -1-1->wf1 5578   -onto->wfo 5579   -1-1-onto->wf1o 5580   ` cfv 5581   omcom 6689   ~~ cen 7563   ~<_ cdom 7564   ~< csdm 7565   Fincfn 7566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-om 6690  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570

This theorem is referenced by:  pssinf  7779  f1finf1o  7795  findcard3  7811  fofinf1o  7849  ackbij1b  8666  fincssdom  8750  fin23lem25  8751  canthp1lem2  9075  pwfseqlem4  9084  uzindi  12191  symggen  17104  pgpssslw  17259  pgpfaclem2  17708  ppiltx  24097  finminlem  30967