Theorem php3 7776

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 7611	. . 3 |- ( A e. Fin <-> E. x e. om A ~~ x )
2		relen 7592	. . . . . . . . 9 |- Rel ~~
3	2	brrelexi 4880	. . . . . . . 8 |- ( A ~~ x -> A e. _V )
4		pssss 3514	. . . . . . . 8 |- ( B C. A -> B C_ A )
5		ssdomg 7633	. . . . . . . . 9 |- ( A e. _V -> ( B C_ A -> B ~<_ A ) )
6	5	imp 436	. . . . . . . 8 |- ( ( A e. _V /\ B C_ A ) -> B ~<_ A )
7	3, 4, 6	syl2an 485	. . . . . . 7 |- ( ( A ~~ x /\ B C. A ) -> B ~<_ A )
8	7	adantll 728	. . . . . 6 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> B ~<_ A )
9		bren 7596	. . . . . . . . 9 |- ( A ~~ x <-> E. f f : A -1-1-onto-> x )
10		imass2 5210	. . . . . . . . . . . . . . . . 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 473	. . . . . . . . . . . . . . 15 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C_ ( f " A ) )
13		pssnel 3829	. . . . . . . . . . . . . . . . 17 |- ( B C. A -> E. y ( y e. A /\ -. y e. B ) )
14		eldif 3400	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( A \ B ) <-> ( y e. A /\ -. y e. B ) )
15		f1ofn 5829	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( f : A -1-1-onto-> x -> f Fn A )
16		difss 3549	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A \ B ) C_ A
17		fnfvima 6161	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( f Fn A /\ ( A \ B ) C_ A /\ y e. ( A \ B ) ) -> ( f ` y ) e. ( f " ( A \ B ) ) )
18	17	3expia 1233	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( f Fn A /\ ( A \ B ) C_ A ) -> ( y e. ( A \ B ) -> ( f ` y ) e. ( f " ( A \ B ) ) ) )
19	15, 16, 18	sylancl 675	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> ( f ` y ) e. ( f " ( A \ B ) ) ) )
20		dff1o3 5834	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( f : A -1-1-onto-> x <-> ( f : A -onto-> x /\ Fun `' f ) )
21	20	simprbi 471	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f : A -1-1-onto-> x -> Fun `' f )
22		imadif 5668	. . . . . . . . . . . . . . . . . . . . . . . 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 2534	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f : A -1-1-onto-> x -> ( ( f ` y ) e. ( f " ( A \ B ) ) <-> ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) ) )
25	19, 24	sylibd 222	. . . . . . . . . . . . . . . . . . . . 21 |- ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) ) )
26		n0i 3727	. . . . . . . . . . . . . . . . . . . . 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 226	. . . . . . . . . . . . . . . . . . 19 |- ( f : A -1-1-onto-> x -> ( ( y e. A /\ -. y e. B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
29	28	exlimdv 1787	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> x -> ( E. y ( y e. A /\ -. y e. B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
30	29	imp 436	. . . . . . . . . . . . . . . . 17 |- ( ( f : A -1-1-onto-> x /\ E. y ( y e. A /\ -. y e. B ) ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
31	13, 30	sylan2 482	. . . . . . . . . . . . . . . 16 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
32		ssdif0 3741	. . . . . . . . . . . . . . . 16 |- ( ( f " A ) C_ ( f " B ) <-> ( ( f " A ) \ ( f " B ) ) = (/) )
33	31, 32	sylnibr 312	. . . . . . . . . . . . . . 15 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> -. ( f " A ) C_ ( f " B ) )
34		dfpss3 3505	. . . . . . . . . . . . . . 15 |- ( ( f " B ) C. ( f " A ) <-> ( ( f " B ) C_ ( f " A ) /\ -. ( f " A ) C_ ( f " B ) ) )
35	12, 33, 34	sylanbrc 677	. . . . . . . . . . . . . 14 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C. ( f " A ) )
36		imadmrn 5184	. . . . . . . . . . . . . . . . 17 |- ( f " dom f ) = ran f
37		f1odm 5832	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> x -> dom f = A )
38	37	imaeq2d 5174	. . . . . . . . . . . . . . . . 17 |- ( f : A -1-1-onto-> x -> ( f " dom f ) = ( f " A ) )
39		f1ofo 5835	. . . . . . . . . . . . . . . . . 18 |- ( f : A -1-1-onto-> x -> f : A -onto-> x )
40		forn 5809	. . . . . . . . . . . . . . . . . 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 2529	. . . . . . . . . . . . . . . 16 |- ( f : A -1-1-onto-> x -> ( f " A ) = x )
43	42	psseq2d 3512	. . . . . . . . . . . . . . 15 |- ( f : A -1-1-onto-> x -> ( ( f " B ) C. ( f " A ) <-> ( f " B ) C. x ) )
44	43	adantr 472	. . . . . . . . . . . . . 14 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( ( f " B ) C. ( f " A ) <-> ( f " B ) C. x ) )
45	35, 44	mpbid 215	. . . . . . . . . . . . 13 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C. x )
46		php 7774	. . . . . . . . . . . . 13 |- ( ( x e. om /\ ( f " B ) C. x ) -> -. x ~~ ( f " B ) )
47	45, 46	sylan2 482	. . . . . . . . . . . 12 |- ( ( x e. om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> -. x ~~ ( f " B ) )
48		f1of1 5827	. . . . . . . . . . . . . . . 16 |- ( f : A -1-1-onto-> x -> f : A -1-1-> x )
49		f1ores 5842	. . . . . . . . . . . . . . . 16 |- ( ( f : A -1-1-> x /\ B C_ A ) -> ( f |` B ) : B -1-1-onto-> ( f " B ) )
50	48, 4, 49	syl2an 485	. . . . . . . . . . . . . . 15 |- ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f |` B ) : B -1-1-onto-> ( f " B ) )
51		vex 3034	. . . . . . . . . . . . . . . . . 18 |- f e. _V
52	51	resex 5154	. . . . . . . . . . . . . . . . 17 |- ( f |` B ) e. _V
53		f1oeq1 5818	. . . . . . . . . . . . . . . . 17 |- ( y = ( f |` B ) -> ( y : B -1-1-onto-> ( f " B ) <-> ( f |` B ) : B -1-1-onto-> ( f " B ) ) )
54	52, 53	spcev 3127	. . . . . . . . . . . . . . . 16 |- ( ( f |` B ) : B -1-1-onto-> ( f " B ) -> E. y y : B -1-1-onto-> ( f " B ) )
55		bren 7596	. . . . . . . . . . . . . . . 16 |- ( B ~~ ( f " B ) <-> E. y y : B -1-1-onto-> ( f " B ) )
56	54, 55	sylibr 217	. . . . . . . . . . . . . . 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 7639	. . . . . . . . . . . . . . 15 |- ( ( x ~~ B /\ B ~~ ( f " B ) ) -> x ~~ ( f " B ) )
59	58	expcom 442	. . . . . . . . . . . . . 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 473	. . . . . . . . . . . 12 |- ( ( x e. om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> ( x ~~ B -> x ~~ ( f " B ) ) )
62	47, 61	mtod 182	. . . . . . . . . . 11 |- ( ( x e. om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> -. x ~~ B )
63	62	exp32 616	. . . . . . . . . 10 |- ( x e. om -> ( f : A -1-1-onto-> x -> ( B C. A -> -. x ~~ B ) ) )
64	63	exlimdv 1787	. . . . . . . . 9 |- ( x e. om -> ( E. f f : A -1-1-onto-> x -> ( B C. A -> -. x ~~ B ) ) )
65	9, 64	syl5bi 225	. . . . . . . 8 |- ( x e. om -> ( A ~~ x -> ( B C. A -> -. x ~~ B ) ) )
66	65	imp31 439	. . . . . . 7 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> -. x ~~ B )
67		entr 7639	. . . . . . . . . 10 |- ( ( B ~~ A /\ A ~~ x ) -> B ~~ x )
68	67	ex 441	. . . . . . . . 9 |- ( B ~~ A -> ( A ~~ x -> B ~~ x ) )
69		ensym 7636	. . . . . . . . 9 |- ( B ~~ x -> x ~~ B )
70	68, 69	syl6com 35	. . . . . . . 8 |- ( A ~~ x -> ( B ~~ A -> x ~~ B ) )
71	70	ad2antlr 741	. . . . . . 7 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> ( B ~~ A -> x ~~ B ) )
72	66, 71	mtod 182	. . . . . 6 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> -. B ~~ A )
73		brsdom 7610	. . . . . 6 |- ( B ~< A <-> ( B ~<_ A /\ -. B ~~ A ) )
74	8, 72, 73	sylanbrc 677	. . . . 5 |- ( ( ( x e. om /\ A ~~ x ) /\ B C. A ) -> B ~< A )
75	74	exp31 615	. . . 4 |- ( x e. om -> ( A ~~ x -> ( B C. A -> B ~< A ) ) )
76	75	rexlimiv 2867	. . 3 |- ( E. x e. om A ~~ x -> ( B C. A -> B ~< A ) )
77	1, 76	sylbi 200	. 2 |- ( A e. Fin -> ( B C. A -> B ~< A ) )
78	77	imp 436	1 |- ( ( A e. Fin /\ B C. A ) -> B ~< A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 376   = wceq 1452   E.wex 1671   e. wcel 1904   E.wrex 2757   _Vcvv 3031   \ cdif 3387   C_ wss 3390   C. wpss 3391   (/)c0 3722   class class class wbr 4395   `'ccnv 4838   dom cdm 4839   ran crn 4840   |` cres 4841   "cima 4842   Fun wfun 5583   Fn wfn 5584   -1-1->wf1 5586   -onto->wfo 5587   -1-1-onto->wf1o 5588   ` cfv 5589   omcom 6711   ~~ cen 7584   ~<_ cdom 7585   ~< csdm 7586   Fincfn 7587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-om 6712  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591

This theorem is referenced by:  pssinf  7800  f1finf1o  7816  findcard3  7832  fofinf1o  7870  ackbij1b  8687  fincssdom  8771  fin23lem25  8772  canthp1lem2  9096  pwfseqlem4  9105  uzindi  12232  symggen  17189  pgpssslw  17344  pgpfaclem2  17793  ppiltx  24183  finminlem  31045