Theorem php3 4580

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 4443	. . 3 |- (A e. Fin <-> E.x e. om A ~~ x)
2		ssdom2g 4470	. . . . . . . . . 10 |- (A e. V -> (B (_ A -> B ~<_ A))
3	2	imp 357	. . . . . . . . 9 |- ((A e. V /\ B (_ A) -> B ~<_ A)
4		relen 4433	. . . . . . . . . 10 |- Rel ~~
5	4	brrelexi 3265	. . . . . . . . 9 |- (A ~~ x -> A e. V)
6		pssss 2194	. . . . . . . . 9 |- (B (. A -> B (_ A)
7	3, 5, 6	syl2an 465	. . . . . . . 8 |- ((A ~~ x /\ B (. A) -> B ~<_ A)
8	7	adantll 401	. . . . . . 7 |- (((x e. om /\ A ~~ x) /\ B (. A) -> B ~<_ A)
9		php 4578	. . . . . . . . . . . . . 14 |- ((x e. om /\ (f"B) (. x) -> -. x ~~ (f"B))
10		imass2 3490	. . . . . . . . . . . . . . . . . . 19 |- (B (_ A -> (f"B) (_ (f"A))
11	6, 10	syl 10	. . . . . . . . . . . . . . . . . 18 |- (B (. A -> (f"B) (_ (f"A))
12	11	adantl 397	. . . . . . . . . . . . . . . . 17 |- ((f:A-1-1-onto->x /\ B (. A) -> (f"B) (_ (f"A))
13		funfvima2 3910	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Fun f /\ (A \ B) (_ dom f) -> (y e. (A \ B) -> (f` y) e. (f"(A \ B))))
14		f1ofun 3748	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:A-1-1-onto->x -> Fun f)
15		difss 2218	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A \ B) (_ A
16		f1ofn 3747	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:A-1-1-onto->x -> f Fn A)
17		fndm 3644	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f Fn A -> dom f = A)
18		sseq2 2134	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 201	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:A-1-1-onto->x -> (A \ B) (_ dom f)
21	13, 14, 20	sylanc 482	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:A-1-1-onto->x -> (y e. (A \ B) -> (f` y) e. (f"(A \ B))))
22		f1o3 3751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:A-1-1-onto->x <-> (f:A-onto->x /\ Fun `'f))
23	22	pm3.27bi 333	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:A-1-1-onto->x -> Fun `'f)
24		imadif 3631	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1588	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:A-1-1-onto->x -> ((f` y) e. (f"(A \ B)) <-> (f` y) e. ((f"A) \ (f"B))))
27	21, 26	sylibd 209	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f:A-1-1-onto->x -> (y e. (A \ B) -> (f` y) e. ((f"A) \ (f"B))))
28		n0i 2336	. . . . . . . . . . . . . . . . . . . . . . 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 2108	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. (A \ B) <-> (y e. A /\ -. y e. B))
31	29, 30	syl5ibr 214	. . . . . . . . . . . . . . . . . . . . 21 |- (f:A-1-1-onto->x -> ((y e. A /\ -. y e. B) -> -. ((f"A) \ (f"B)) = (/)))
32	31	19.23adv 1256	. . . . . . . . . . . . . . . . . . . 20 |- (f:A-1-1-onto->x -> (E.y(y e. A /\ -. y e. B) -> -. ((f"A) \ (f"B)) = (/)))
33	32	imp 357	. . . . . . . . . . . . . . . . . . 19 |- ((f:A-1-1-onto->x /\ E.y(y e. A /\ -. y e. B)) -> -. ((f"A) \ (f"B)) = (/))
34		pssnel 2383	. . . . . . . . . . . . . . . . . . 19 |- (B (. A -> E.y(y e. A /\ -. y e. B))
35	33, 34	sylan2 462	. . . . . . . . . . . . . . . . . 18 |- ((f:A-1-1-onto->x /\ B (. A) -> -. ((f"A) \ (f"B)) = (/))
36		ssdif0 2379	. . . . . . . . . . . . . . . . . . 19 |- ((f"A) (_ (f"B) <-> ((f"A) \ (f"B)) = (/))
37	36	notbii 194	. . . . . . . . . . . . . . . . . 18 |- (-. (f"A) (_ (f"B) <-> -. ((f"A) \ (f"B)) = (/))
38	35, 37	sylibr 207	. . . . . . . . . . . . . . . . 17 |- ((f:A-1-1-onto->x /\ B (. A) -> -. (f"A) (_ (f"B))
39	12, 38	jca 295	. . . . . . . . . . . . . . . 16 |- ((f:A-1-1-onto->x /\ B (. A) -> ((f"B) (_ (f"A) /\ -. (f"A) (_ (f"B)))
40		dfpss3 2185	. . . . . . . . . . . . . . . 16 |- ((f"B) (. (f"A) <-> ((f"B) (_ (f"A) /\ -. (f"A) (_ (f"B)))
41	39, 40	sylibr 207	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->x /\ B (. A) -> (f"B) (. (f"A))
42		imadmrn 3471	. . . . . . . . . . . . . . . . . . 19 |- (f"dom f) = ran f
43	42	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (f:A-1-1-onto->x -> (f"dom f) = ran f)
44		imaeq2 3459	. . . . . . . . . . . . . . . . . . 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 3752	. . . . . . . . . . . . . . . . . . 19 |- (f:A-1-1-onto->x -> f:A-onto->x)
47		forn 3731	. . . . . . . . . . . . . . . . . . 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 1562	. . . . . . . . . . . . . . . . 17 |- (f:A-1-1-onto->x -> (f"A) = x)
50	49	psseq2d 2192	. . . . . . . . . . . . . . . 16 |- (f:A-1-1-onto->x -> ((f"B) (. (f"A) <-> (f"B) (. x))
51	50	adantr 398	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->x /\ B (. A) -> ((f"B) (. (f"A) <-> (f"B) (. x))
52	41, 51	mpbid 202	. . . . . . . . . . . . . 14 |- ((f:A-1-1-onto->x /\ B (. A) -> (f"B) (. x)
53	9, 52	sylan2 462	. . . . . . . . . . . . 13 |- ((x e. om /\ (f:A-1-1-onto->x /\ B (. A)) -> -. x ~~ (f"B))
54		f1ores 3760	. . . . . . . . . . . . . . . 16 |- ((f:A-1-1->x /\ B (_ A) -> (f |` B):B-1-1-onto->(f"B))
55		f1of1 3745	. . . . . . . . . . . . . . . 16 |- (f:A-1-1-onto->x -> f:A-1-1->x)
56	54, 55, 6	syl2an 465	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->x /\ B (. A) -> (f |` B):B-1-1-onto->(f"B))
57		visset 1860	. . . . . . . . . . . . . . . . . 18 |- f e. V
58		resexg 3451	. . . . . . . . . . . . . . . . . 18 |- (f e. V -> (f |` B) e. V)
59	57, 58	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (f |` B) e. V
60		f1oeq1 3741	. . . . . . . . . . . . . . . . 17 |- (y = (f |` B) -> (y:B-1-1-onto->(f"B) <-> (f |` B):B-1-1-onto->(f"B)))
61	59, 60	cla4ev 1916	. . . . . . . . . . . . . . . 16 |- ((f |` B):B-1-1-onto->(f"B) -> E.y y:B-1-1-onto->(f"B))
62		imaexg 3473	. . . . . . . . . . . . . . . . . 18 |- (f e. V -> (f"B) e. V)
63	57, 62	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (f"B) e. V
64	63	bren 4438	. . . . . . . . . . . . . . . 16 |- (B ~~ (f"B) <-> E.y y:B-1-1-onto->(f"B))
65	61, 64	sylibr 207	. . . . . . . . . . . . . . 15 |- ((f |` B):B-1-1-onto->(f"B) -> B ~~ (f"B))
66		entr 4475	. . . . . . . . . . . . . . . 16 |- ((x ~~ B /\ B ~~ (f"B)) -> x ~~ (f"B))
67	66	expcom 381	. . . . . . . . . . . . . . 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 397	. . . . . . . . . . . . 13 |- ((x e. om /\ (f:A-1-1-onto->x /\ B (. A)) -> (x ~~ B -> x ~~ (f"B)))
70	53, 69	mtod 114	. . . . . . . . . . . 12 |- ((x e. om /\ (f:A-1-1-onto->x /\ B (. A)) -> -. x ~~ B)
71	70	exp32 386	. . . . . . . . . . 11 |- (x e. om -> (f:A-1-1-onto->x -> (B (. A -> -. x ~~ B)))
72	71	19.23adv 1256	. . . . . . . . . 10 |- (x e. om -> (E.f f:A-1-1-onto->x -> (B (. A -> -. x ~~ B)))
73		visset 1860	. . . . . . . . . . 11 |- x e. V
74	73	bren 4438	. . . . . . . . . 10 |- (A ~~ x <-> E.f f:A-1-1-onto->x)
75	72, 74	syl5ib 213	. . . . . . . . 9 |- (x e. om -> (A ~~ x -> (B (. A -> -. x ~~ B)))
76	75	imp31 369	. . . . . . . 8 |- (((x e. om /\ A ~~ x) /\ B (. A) -> -. x ~~ B)
77		entr 4475	. . . . . . . . . . 11 |- ((B ~~ A /\ A ~~ x) -> B ~~ x)
78	77	ex 380	. . . . . . . . . 10 |- (B ~~ A -> (A ~~ x -> B ~~ x))
79	73	ensym 4473	. . . . . . . . . 10 |- (B ~~ x -> x ~~ B)
80	78, 79	syl6com 53	. . . . . . . . 9 |- (A ~~ x -> (B ~~ A -> x ~~ B))
81	80	ad2antlr 414	. . . . . . . 8 |- (((x e. om /\ A ~~ x) /\ B (. A) -> (B ~~ A -> x ~~ B))
82	76, 81	mtod 114	. . . . . . 7 |- (((x e. om <