Theorem php3 4662

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.

Assertion

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

Proof of Theorem php3

Step	Hyp	Ref	Expression
1		isfi 4523	. . 3 |- (A e. Fin <-> E.x e. om A ~~ x)
2		ssdom2g 4550	. . . . . . . . . 10 |- (A e. V -> (B (_ A -> B ~<_ A))
3	2	imp 348	. . . . . . . . 9 |- ((A e. V /\ B (_ A) -> B ~<_ A)
4		relen 4513	. . . . . . . . . 10 |- Rel ~~
5	4	brrelexi 3291	. . . . . . . . 9 |- (A ~~ x -> A e. V)
6		pssss 2195	. . . . . . . . 9 |- (B (. A -> B (_ A)
7	3, 5, 6	syl2an 456	. . . . . . . 8 |- ((A ~~ x /\ B (. A) -> B ~<_ A)
8	7	adantll 392	. . . . . . 7 |- (((x e. om /\ A ~~ x) /\ B (. A) -> B ~<_ A)
9		php 4660	. . . . . . . . . . . . . 14 |- ((x e. om /\ (f"B) (. x) -> -. x ~~ (f"B))
10		imass2 3525	. . . . . . . . . . . . . . . . . . 19 |- (B (_ A -> (f"B) (_ (f"A))
11	6, 10	syl 10	. . . . . . . . . . . . . . . . . 18 |- (B (. A -> (f"B) (_ (f"A))
12	11	adantl 388	. . . . . . . . . . . . . . . . 17 |- ((f:A-1-1-onto->x /\ B (. A) -> (f"B) (_ (f"A))
13		funfvima2 3967	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Fun f /\ (A \ B) (_ dom f) -> (y e. (A \ B) -> (f` y) e. (f"(A \ B))))
14		f1ofun 3799	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:A-1-1-onto->x -> Fun f)
15		difss 2219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A \ B) (_ A
16		f1ofn 3798	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:A-1-1-onto->x -> f Fn A)
17		fndm 3693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f Fn A -> dom f = A)
18		sseq2 2135	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (dom f = A -> ((A \ B) (_ dom f <-> (A \ B) (_ A))
19	16, 17, 18	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:A-1-1-onto->x -> ((A \ B) (_ dom f <-> (A \ B) (_ A))
20	15, 19	mpbiri 192	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:A-1-1-onto->x -> (A \ B) (_ dom f)
21	13, 14, 20	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:A-1-1-onto->x -> (y e. (A \ B) -> (f` y) e. (f"(A \ B))))
22		dff1o3 3802	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:A-1-1-onto->x <-> (f:A-onto->x /\ Fun `'f))
23	22	pm3.27bi 324	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:A-1-1-onto->x -> Fun `'f)
24		imadif 3679	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (Fun `'f -> (f"(A \ B)) = ((f"A) \ (f"B)))
25	23, 24	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:A-1-1-onto->x -> (f"(A \ B)) = ((f"A) \ (f"B)))
26	25	eleq2d 1584	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:A-1-1-onto->x -> ((f` y) e. (f"(A \ B)) <-> (f` y) e. ((f"A) \ (f"B))))
27	21, 26	sylibd 200	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f:A-1-1-onto->x -> (y e. (A \ B) -> (f` y) e. ((f"A) \ (f"B))))
28		n0i 2337	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f` y) e. ((f"A) \ (f"B)) -> -. ((f"A) \ (f"B)) = (/))
29	27, 28	syl6 22	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:A-1-1-onto->x -> (y e. (A \ B) -> -. ((f"A) \ (f"B)) = (/)))
30		eldif 2109	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. (A \ B) <-> (y e. A /\ -. y e. B))
31	29, 30	syl5ibr 205	. . . . . . . . . . . . . . . . . . . . 21 |- (f:A-1-1-onto->x -> ((y e. A /\ -. y e. B) -> -. ((f"A) \ (f"B)) = (/)))
32	31	19.23adv 1251	. . . . . . . . . . . . . . . . . . . 20 |- (f:A-1-1-onto->x -> (E.y(y e. A /\ -. y e. B) -> -. ((f"A) \ (f"B)) = (/)))
33	32	imp 348	. . . . . . . . . . . . . . . . . . 19 |- ((f:A-1-1-onto->x /\ E.y(y e. A /\ -. y e. B)) -> -. ((f"A) \ (f"B)) = (/))
34		pssnel 2384	. . . . . . . . . . . . . . . . . . 19 |- (B (. A -> E.y(y e. A /\ -. y e. B))
35	33, 34	sylan2 453	. . . . . . . . . . . . . . . . . 18 |- ((f:A-1-1-onto->x /\ B (. A) -> -. ((f"A) \ (f"B)) = (/))
36		ssdif0 2380	. . . . . . . . . . . . . . . . . . 19 |- ((f"A) (_ (f"B) <-> ((f"A) \ (f"B)) = (/))
37	36	notbii 185	. . . . . . . . . . . . . . . . . 18 |- (-. (f"A) (_ (f"B) <-> -. ((f"A) \ (f"B)) = (/))
38	35, 37	sylibr 198	. . . . . . . . . . . . . . . . 17 |- ((f:A-1-1-onto->x /\ B (. A) -> -. (f"A) (_ (f"B))
39	12, 38	jca 286	. . . . . . . . . . . . . . . 16 |- ((f:A-1-1-onto->x /\ B (. A) -> ((f"B) (_ (f"A) /\ -. (f"A) (_ (f"B)))
40		dfpss3 2186	. . . . . . . . . . . . . . . 16 |- ((f"B) (. (f"A) <-> ((f"B) (_ (f"A) /\ -. (f"A) (_ (f"B)))
41	39, 40	sylibr 198	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->x /\ B (. A) -> (f"B) (. (f"A))
42		imadmrn 3506	. . . . . . . . . . . . . . . . . . 19 |- (f"dom f) = ran f
43	42	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (f:A-1-1-onto->x -> (f"dom f) = ran f)
44		imaeq2 3492	. . . . . . . . . . . . . . . . . . 19 |- (dom f = A -> (f"dom f) = (f"A))
45	16, 17, 44	3syl 20	. . . . . . . . . . . . . . . . . 18 |- (f:A-1-1-onto->x -> (f"dom f) = (f"A))
46		f1ofo 3803	. . . . . . . . . . . . . . . . . . 19 |- (f:A-1-1-onto->x -> f:A-onto->x)
47		forn 3782	. . . . . . . . . . . . . . . . . . 19 |- (f:A-onto->x -> ran f = x)
48	46, 47	syl 10	. . . . . . . . . . . . . . . . . 18 |- (f:A-1-1-onto->x -> ran f = x)
49	43, 45, 48	3eqtr3d 1558	. . . . . . . . . . . . . . . . 17 |- (f:A-1-1-onto->x -> (f"A) = x)
50	49	psseq2d 2193	. . . . . . . . . . . . . . . 16 |- (f:A-1-1-onto->x -> ((f"B) (. (f"A) <-> (f"B) (. x))
51	50	adantr 389	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->x /\ B (. A) -> ((f"B) (. (f"A) <-> (f"B) (. x))
52	41, 51	mpbid 193	. . . . . . . . . . . . . 14 |- ((f:A-1-1-onto->x /\ B (. A) -> (f"B) (. x)
53	9, 52	sylan2 453	. . . . . . . . . . . . 13 |- ((x e. om /\ (f:A-1-1-onto->x /\ B (. A)) -> -. x ~~ (f"B))
54		f1ores 3811	. . . . . . . . . . . . . . . 16 |- ((f:A-1-1->x /\ B (_ A) -> (f |` B):B-1-1-onto->(f"B))
55		f1of1 3796	. . . . . . . . . . . . . . . 16 |- (f:A-1-1-onto->x -> f:A-1-1->x)
56	54, 55, 6	syl2an 456	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->x /\ B (. A) -> (f |` B):B-1-1-onto->(f"B))
57		visset 1859	. . . . . . . . . . . . . . . . . 18 |- f e. V
58		resexg 3484	. . . . . . . . . . . . . . . . . 18 |- (f e. V -> (f |` B) e. V)
59	57, 58	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (f |` B) e. V
60		f1oeq1 3792	. . . . . . . . . . . . . . . . 17 |- (y = (f |` B) -> (y:B-1-1-onto->(f"B) <-> (f |` B):B-1-1-onto->(f"B)))
61	59, 60	cla4ev 1915	. . . . . . . . . . . . . . . 16 |- ((f |` B):B-1-1-onto->(f"B) -> E.y y:B-1-1-onto->(f"B))
62		imaexg 3508	. . . . . . . . . . . . . . . . . 18 |- (f e. V -> (f"B) e. V)
63	57, 62	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (f"B) e. V
64	63	bren 4518	. . . . . . . . . . . . . . . 16 |- (B ~~ (f"B) <-> E.y y:B-1-1-onto->(f"B))
65	61, 64	sylibr 198	. . . . . . . . . . . . . . 15 |- ((f |` B):B-1-1-onto->(f"B) -> B ~~ (f"B))
66		entr 4555	. . . . . . . . . . . . . . . 16 |- ((x ~~ B /\ B ~~ (f"B)) -> x ~~ (f"B))
67	66	expcom 372	. . . . . . . . . . . . . . 15 |- (B ~~ (f"B) -> (x ~~ B -> x ~~ (f"B)))
68	56, 65, 67	3syl 20	. . . . . . . . . . . . . 14 |- ((f:A-1-1-onto->x /\ B (. A) -> (x ~~ B -> x ~~ (f"B)))
69	68	adantl 388	. . . . . . . . . . . . 13 |- ((x e. om /\ (f:A-1-1-onto->x /\ B (. A)) -> (x ~~ B -> x ~~ (f"B)))
70	53, 69	mtod 107	. . . . . . . . . . . 12 |- ((x e. om /\ (f:A-1-1-onto->x /\ B (. A)) -> -. x ~~ B)
71	70	exp32 377	. . . . . . . . . . 11 |- (x e. om -> (f:A-1-1-onto->x -> (B (. A -> -. x ~~ B)))
72	71	19.23adv 1251	. . . . . . . . . 10 |- (x e. om -> (E.f f:A-1-1-onto->x -> (B (. A -> -. x ~~ B)))
73		visset 1859	. . . . . . . . . . 11 |- x e. V
74	73	bren 4518	. . . . . . . . . 10 |- (A ~~ x <-> E.f f:A-1-1-onto->x)
75	72, 74	syl5ib 204	. . . . . . . . 9 |- (x e. om -> (A ~~ x -> (B (. A -> -. x ~~ B)))
76	75	imp31 360	. . . . . . . 8 |- (((x e. om /\ A ~~ x) /\ B (. A) -> -. x ~~ B)
77		entr 4555	. . . . . . . . . . 11 |- ((B ~~ A /\ A ~~ x) -> B ~~ x)
78	77	ex 371	. . . . . . . . . 10 |- (B ~~ A -> (A ~~ x -> B ~~ x))
79	73	ensym 4553	. . . . . . . . . 10 |- (B ~~ x -> x ~~ B)
80	78, 79	syl6com 53	. . . . . . . . 9 |- (A ~~ x -> (B ~~ A -> x ~~ B))
81	80	ad2antlr 405	. . . . . . . 8 |- (((x e. om /\ A ~~ x) /\ B (. A) -> (B ~~ A -> x ~~ B))
82	76, 81	mtod 107	. . . . . . 7 |- (((x e. om /\ A ~~ x) /\ B (. A) -> -. B ~~ A)
83	8, 82	jca 286	. . . . . 6 |- (((x e. om /\ A ~~ x) /\ B (. A) -> (B ~<_ A /\ -. B ~~ A))
84		brsdom 4522	. . . . . 6 |- (B ~< A <-> (B ~<_ A /\ -. B ~~ A))
85	83, 84	sylibr 198	. . . . 5 |- (((x e. om /\ A ~~ x) /\ B (. A) -> B ~< A)
86	85	exp31 376	. . . 4 |- (x e. om -> (A ~~ x -> (B (. A -> B ~< A)))
87	86	r19.23aiv 1789	. . 3 |- (E.x e. om A ~~ x -> (B (. A -> B ~< A))
88	1, 87	sylbi 197	. 2 |- (A e. Fin -> (B (. A -> B ~< A))
89	88	imp 348	1 |- ((A e. Fin /\ B (. A) -> B ~< A)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   /\ wa 221   = wceq 992   e. wcel 994  E.wex 1016  E.wrex 1692  Vcvv 1857   \ cdif 2096   (_ wss 2099   (. wpss 2100  (/)c0 2332   class class class wbr 2692  omcom 3218  `'ccnv 3250  dom cdm 3251  ran crn 3252   |` cres 3253  "cima 3254  Fun wfun 3257   Fn wfn 3258  -1-1->wf1 3260  -onto->wfo 3261  -1-1-onto->wf1o 3262  ` cfv 3263   ~~ cen 4505   ~<_ cdom 4506   ~< csdm 4507  Fincfn 4508

This theorem is referenced by:  pssinf 4674  finminlem 11418

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-pss 2107  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-er 4401  df-en 4509  df-dom 4510  df-sdom 4511  df-fin 4512

Copyright terms: Public domain