Theorem php3 7741

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 7577	. . 3 |- ( A e. Fin <-> E. x e. om A ~~ x )
2		relen 7559	. . . . . . . . 9 |- Rel ~~
3	2	brrelexi 4864	. . . . . . . 8 |- ( A ~~ x -> A e. _V )
4		pssss 3538	. . . . . . . 8 |- ( B C. A -> B C_ A )
5		ssdomg 7599	. . . . . . . . 9 |- ( A e. _V -> ( B C_ A -> B ~<_ A ) )
6	5	imp 427	. . . . . . . 8 |- ( ( A e. _V /\ B C_ A ) -> B ~<_ A )
7	3, 4, 6	syl2an 475	. . . . . . 7 |- ( ( A ~~ x /\ B C. A ) -> B ~<_ A )
8	7	adantll 712	. . . . . 6 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> B ~<_ A )
9		bren 7563	. . . . . . . . 9 |- ( A ~~ x <-> E. f f : A -1-1-onto-> x )
10		imass2 5192	. . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . 15 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C_ ( f " A ) )
13		pssnel 3837	. . . . . . . . . . . . . . . . 17 |- ( B C. A -> E. y ( y e. A /\ -. y e. B ) )
14		eldif 3424	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( A \ B ) <-> ( y e. A /\ -. y e. B ) )
15		f1ofn 5800	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( f : A -1-1-onto-> x -> f Fn A )
16		difss 3570	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A \ B ) C_ A
17		fnfvima 6131	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f Fn A /\ ( A \ B ) C_ A /\ y e. ( A \ B ) ) -> ( f ` y ) e. ( f " ( A \ B ) ) )
18	17	3expia 1199	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( f Fn A /\ ( A \ B ) C_ A ) -> ( y e. ( A \ B ) -> ( f ` y ) e. ( f " ( A \ B ) ) ) )
19	15, 16, 18	sylancl 660	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> ( f ` y ) e. ( f " ( A \ B ) ) ) )
20		dff1o3 5805	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : A -1-1-onto-> x <-> ( f : A -onto-> x /\ Fun `' f ) )
21	20	simprbi 462	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f : A -1-1-onto-> x -> Fun `' f )
22		imadif 5644	. . . . . . . . . . . . . . . . . . . . . . . 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 2472	. . . . . . . . . . . . . . . . . . . . . 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 3743	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
27	25, 26	syl6 31	. . . . . . . . . . . . . . . . . . . 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 1745	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> x -> ( E. y ( y e. A /\ -. y e. B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
30	29	imp 427	. . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-onto-> x /\ E. y ( y e. A /\ -. y e. B ) ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
31	13, 30	sylan2 472	. . . . . . . . . . . . . . . 16 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
32		ssdif0 3828	. . . . . . . . . . . . . . . 16 |- ( ( f " A ) C_ ( f " B ) <-> ( ( f " A ) \ ( f " B ) ) = (/) )
33	31, 32	sylnibr 303	. . . . . . . . . . . . . . 15 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> -. ( f " A ) C_ ( f " B ) )
34		dfpss3 3529	. . . . . . . . . . . . . . 15 |- ( ( f " B ) C. ( f " A ) <-> ( ( f " B ) C_ ( f " A ) /\ -. ( f " A ) C_ ( f " B ) ) )
35	12, 33, 34	sylanbrc 662	. . . . . . . . . . . . . 14 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C. ( f " A ) )
36		imadmrn 5167	. . . . . . . . . . . . . . . . 17 |- ( f " dom f ) = ran f
37		f1odm 5803	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> x -> dom f = A )
38	37	imaeq2d 5157	. . . . . . . . . . . . . . . . 17 |- ( f : A -1-1-onto-> x -> ( f " dom f ) = ( f " A ) )
39		f1ofo 5806	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> x -> f : A -onto-> x )
40		forn 5781	. . . . . . . . . . . . . . . . . 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 2467	. . . . . . . . . . . . . . . 16 |- ( f : A -1-1-onto-> x -> ( f " A ) = x )
43	42	psseq2d 3536	. . . . . . . . . . . . . . 15 |- ( f : A -1-1-onto-> x -> ( ( f " B ) C. ( f " A ) <-> ( f " B ) C. x ) )
44	43	adantr 463	. . . . . . . . . . . . . 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 7739	. . . . . . . . . . . . 13 |- ( ( x e. om /\ ( f " B ) C. x ) -> -. x ~~ ( f " B ) )
47	45, 46	sylan2 472	. . . . . . . . . . . 12 |- ( ( x e. om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> -. x ~~ ( f " B ) )
48		f1of1 5798	. . . . . . . . . . . . . . . 16 |- ( f : A -1-1-onto-> x -> f : A -1-1-> x )
49		f1ores 5813	. . . . . . . . . . . . . . . 16 |- ( ( f : A -1-1-> x /\ B C_ A ) -> ( f |` B ) : B -1-1-onto-> ( f " B ) )
50	48, 4, 49	syl2an 475	. . . . . . . . . . . . . . 15 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f |` B ) : B -1-1-onto-> ( f " B ) )
51		vex 3062	. . . . . . . . . . . . . . . . . 18 |- f e. _V
52	51	resex 5137	. . . . . . . . . . . . . . . . 17 |- ( f |` B ) e. _V
53		f1oeq1 5790	. . . . . . . . . . . . . . . . 17 |- ( y = ( f |` B ) -> ( y : B -1-1-onto-> ( f " B ) <-> ( f |` B ) : B -1-1-onto-> ( f " B ) ) )
54	52, 53	spcev 3151	. . . . . . . . . . . . . . . 16 |- ( ( f |` B ) : B -1-1-onto-> ( f " B ) -> E. y y : B -1-1-onto-> ( f " B ) )
55		bren 7563	. . . . . . . . . . . . . . . 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 17	. . . . . . . . . . . . . 14 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> B ~~ ( f " B ) )
58		entr 7605	. . . . . . . . . . . . . . 15 |- ( ( x ~~ B /\ B ~~ ( f " B ) ) -> x ~~ ( f " B ) )
59	58	expcom 433	. . . . . . . . . . . . . 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 464	. . . . . . . . . . . 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 603	. . . . . . . . . 10 |- ( x e. om -> ( f : A -1-1-onto-> x -> ( B C. A -> -. x ~~ B ) ) )
64	63	exlimdv 1745	. . . . . . . . 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 430	. . . . . . 7 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> -. x ~~ B )
67		entr 7605	. . . . . . . . . 10 |- ( ( B ~~ A /\ A ~~ x ) -> B ~~ x )
68	67	ex 432	. . . . . . . . 9 |- ( B ~~ A -> ( A ~~ x -> B ~~ x ) )
69		ensym 7602	. . . . . . . . 9 |- ( B ~~ x -> x ~~ B )
70	68, 69	syl6com 33	. . . . . . . 8 |- ( A ~~ x -> ( B ~~ A -> x ~~ B ) )
71	70	ad2antlr 725	. . . . . . 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 7576	. . . . . 6 |- ( B ~< A <-> ( B ~<_ A /\ -. B ~~ A ) )
74	8, 72, 73	sylanbrc 662	. . . . 5 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> B ~< A )
75	74	exp31 602	. . . 4 |- ( x e. om -> ( A ~~ x -> ( B C. A -> B ~< A ) ) )
76	75	rexlimiv 2890	. . 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 427	1 |- ( ( A e. Fin /\ B C. A ) -> B ~< A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1405   E.wex 1633   e. wcel 1842   E.wrex 2755   _Vcvv 3059   \ cdif 3411   C_ wss 3414   C. wpss 3415   (/)c0 3738   class class class wbr 4395   `'ccnv 4822   dom cdm 4823   ran crn 4824   |` cres 4825   "cima 4826   Fun wfun 5563   Fn wfn 5564   -1-1->wf1 5566   -onto->wfo 5567   -1-1-onto->wf1o 5568   ` cfv 5569   omcom 6683   ~~ cen 7551   ~<_ cdom 7552   ~< csdm 7553   Fincfn 7554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-sbc 3278  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-om 6684  df-er 7348  df-en 7555  df-dom 7556  df-sdom 7557  df-fin 7558

This theorem is referenced by:  pssinf  7765  f1finf1o  7781  findcard3  7797  fofinf1o  7835  ackbij1b  8651  fincssdom  8735  fin23lem25  8736  canthp1lem2  9061  pwfseqlem4  9070  uzindi  12132  symggen  16819  pgpssslw  16958  pgpfaclem2  17453  ppiltx  23832  finminlem  30546