Theorem php3 3411

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. (The expression E.x e. omA ~~ x is the definition of "finite", and "infinite" is defined as "not finite".)

Assertion

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

Distinct variable group(s):   x,A

Proof of Theorem php3

Step	Hyp	Ref	Expression
1		ssdom2g 3312	. . . . . . . . . 10 |- (A e. V -> (B (_ A -> B ~<_ A))
2	1	imp 277	. . . . . . . . 9 |- ((A e. V /\ B (_ A) -> B ~<_ A)
3		relen 3277	. . . . . . . . . 10 |- Rel ~~
4	3	brrelexi 2447	. . . . . . . . 9 |- (A ~~ z -> A e. V)
5		pssss 1567	. . . . . . . . 9 |- (B (. A -> B (_ A)
6	2, 4, 5	syl2an 349	. . . . . . . 8 |- ((A ~~ z /\ B (. A) -> B ~<_ A)
7	6	adantll 309	. . . . . . 7 |- (((z e. om /\ A ~~ z) /\ B (. A) -> B ~<_ A)
8		php 3409	. . . . . . . . . . . . . 14 |- ((z e. om /\ (f"B) (. z) -> -. z ~~ (f"B))
9		imass2 2622	. . . . . . . . . . . . . . . . . . 19 |- (B (_ A -> (f"B) (_ (f"A))
10	5, 9	syl 12	. . . . . . . . . . . . . . . . . 18 |- (B (. A -> (f"B) (_ (f"A))
11	10	adantl 305	. . . . . . . . . . . . . . . . 17 |- ((f:A-1-1-onto->z /\ B (. A) -> (f"B) (_ (f"A))
12		funfvima2 2905	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Fun f /\ (A \ B) (_ dom f) -> (y e. (A \ B) -> (f` y) e. (f"(A \ B))))
13		f1ofun 2802	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:A-1-1-onto->z -> Fun f)
14		difss 1596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A \ B) (_ A
15		f1ofn 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:A-1-1-onto->z -> f Fn A)
16		fndm 2723	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f Fn A -> dom f = A)
17		sseq2 1522	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (dom f = A -> ((A \ B) (_ dom f <-> (A \ B) (_ A))
18	15, 16, 17	3syl 21	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:A-1-1-onto->z -> ((A \ B) (_ dom f <-> (A \ B) (_ A))
19	14, 18	mpbiri 169	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:A-1-1-onto->z -> (A \ B) (_ dom f)
20	12, 13, 19	sylanc 361	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:A-1-1-onto->z -> (y e. (A \ B) -> (f` y) e. (f"(A \ B))))
21		f1o3 2805	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:A-1-1-onto->z <-> (f:A-onto->z /\ Fun `'f))
22	21	pm3.27bd 263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:A-1-1-onto->z -> Fun `'f)
23		imadif 2714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (Fun `'f -> (f"(A \ B)) = ((f"A) \ (f"B)))
24	22, 23	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:A-1-1-onto->z -> (f"(A \ B)) = ((f"A) \ (f"B)))
25	24	eleq2d 1156	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:A-1-1-onto->z -> ((f` y) e. (f"(A \ B)) <-> (f` y) e. ((f"A) \ (f"B))))
26	20, 25	sylibd 177	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f:A-1-1-onto->z -> (y e. (A \ B) -> (f` y) e. ((f"A) \ (f"B))))
27		n0i 1712	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f` y) e. ((f"A) \ (f"B)) -> -. ((f"A) \ (f"B)) = (/))
28	26, 27	syl6 23	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:A-1-1-onto->z -> (y e. (A \ B) -> -. ((f"A) \ (f"B)) = (/)))
29		eldif 1496	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. (A \ B) <-> (y e. A /\ -. y e. B))
30	28, 29	syl5ibr 182	. . . . . . . . . . . . . . . . . . . . 21 |- (f:A-1-1-onto->z -> ((y e. A /\ -. y e. B) -> -. ((f"A) \ (f"B)) = (/)))
31	30	19.23adv 954	. . . . . . . . . . . . . . . . . . . 20 |- (f:A-1-1-onto->z -> (E.y(y e. A /\ -. y e. B) -> -. ((f"A) \ (f"B)) = (/)))
32	31	imp 277	. . . . . . . . . . . . . . . . . . 19 |- ((f:A-1-1-onto->z /\ E.y(y e. A /\ -. y e. B)) -> -. ((f"A) \ (f"B)) = (/))
33		pssnel 1752	. . . . . . . . . . . . . . . . . . 19 |- (B (. A -> E.y(y e. A /\ -. y e. B))
34	32, 33	sylan2 346	. . . . . . . . . . . . . . . . . 18 |- ((f:A-1-1-onto->z /\ B (. A) -> -. ((f"A) \ (f"B)) = (/))
35		ssdif0 1748	. . . . . . . . . . . . . . . . . . 19 |- ((f"A) (_ (f"B) <-> ((f"A) \ (f"B)) = (/))
36	35	negbii 162	. . . . . . . . . . . . . . . . . 18 |- (-. (f"A) (_ (f"B) <-> -. ((f"A) \ (f"B)) = (/))
37	34, 36	sylibr 175	. . . . . . . . . . . . . . . . 17 |- ((f:A-1-1-onto->z /\ B (. A) -> -. (f"A) (_ (f"B))
38	11, 37	jca 236	. . . . . . . . . . . . . . . 16 |- ((f:A-1-1-onto->z /\ B (. A) -> ((f"B) (_ (f"A) /\ -. (f"A) (_ (f"B)))
39		dfpss3 1558	. . . . . . . . . . . . . . . 16 |- ((f"B) (. (f"A) <-> ((f"B) (_ (f"A) /\ -. (f"A) (_ (f"B)))
40	38, 39	sylibr 175	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->z /\ B (. A) -> (f"B) (. (f"A))
41		imadmrn 2610	. . . . . . . . . . . . . . . . . . 19 |- (f"dom f) = ran f
42	41	a1i 7	. . . . . . . . . . . . . . . . . 18 |- (f:A-1-1-onto->z -> (f"dom f) = ran f)
43		imaeq2 2603	. . . . . . . . . . . . . . . . . . 19 |- (dom f = A -> (f"dom f) = (f"A))
44	15, 16, 43	3syl 21	. . . . . . . . . . . . . . . . . 18 |- (f:A-1-1-onto->z -> (f"dom f) = (f"A))
45		f1ofo 2806	. . . . . . . . . . . . . . . . . . 19 |- (f:A-1-1-onto->z -> f:A-onto->z)
46		forn 2789	. . . . . . . . . . . . . . . . . . 19 |- (f:A-onto->z -> ran f = z)
47	45, 46	syl 12	. . . . . . . . . . . . . . . . . 18 |- (f:A-1-1-onto->z -> ran f = z)
48	42, 44, 47	3eqtr3d 1133	. . . . . . . . . . . . . . . . 17 |- (f:A-1-1-onto->z -> (f"A) = z)
49	48	psseq2d 1565	. . . . . . . . . . . . . . . 16 |- (f:A-1-1-onto->z -> ((f"B) (. (f"A) <-> (f"B) (. z))
50	49	adantr 306	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->z /\ B (. A) -> ((f"B) (. (f"A) <-> (f"B) (. z))
51	40, 50	mpbid 170	. . . . . . . . . . . . . 14 |- ((f:A-1-1-onto->z /\ B (. A) -> (f"B) (. z)
52	8, 51	sylan2 346	. . . . . . . . . . . . 13 |- ((z e. om /\ (f:A-1-1-onto->z /\ B (. A)) -> -. z ~~ (f"B))
53		f1ores 2813	. . . . . . . . . . . . . . . 16 |- ((f:A-1-1->z /\ B (_ A) -> (f |` B):B-1-1-onto->(f"B))
54		f1of1 2799	. . . . . . . . . . . . . . . 16 |- (f:A-1-1-onto->z -> f:A-1-1->z)
55	53, 54, 5	syl2an 349	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->z /\ B (. A) -> (f |` B):B-1-1-onto->(f"B))
56		visset 1350	. . . . . . . . . . . . . . . . . 18 |- f e. V
57		resexg 2597	. . . . . . . . . . . . . . . . . 18 |- (f e. V -> (f |` B) e. V)
58	56, 57	ax-mp 6	. . . . . . . . . . . . . . . . 17 |- (f |` B) e. V
59		f1oeq1 2795	. . . . . . . . . . . . . . . . 17 |- (y = (f |` B) -> (y:B-1-1-onto->(f"B) <-> (f |` B):B-1-1-onto->(f"B)))
60	58, 59	cla4ev 1401	. . . . . . . . . . . . . . . 16 |- ((f |` B):B-1-1-onto->(f"B) -> E.y y:B-1-1-onto->(f"B))
61		imaexg 2612	. . . . . . . . . . . . . . . . . 18 |- (f e. V -> (f"B) e. V)
62	56, 61	ax-mp 6	. . . . . . . . . . . . . . . . 17 |- (f"B) e. V
63	62	bren 3282	. . . . . . . . . . . . . . . 16 |- (B ~~ (f"B) <-> E.y y:B-1-1-onto->(f"B))
64	60, 63	sylibr 175	. . . . . . . . . . . . . . 15 |- ((f |` B):B-1-1-onto->(f"B) -> B ~~ (f"B))
65		entrt 3319	. . . . . . . . . . . . . . . . 17 |- ((z ~~ B /\ B ~~ (f"B)) -> z ~~ (f"B))
66	65	exp 291	. . . . . . . . . . . . . . . 16 |- (z ~~ B -> (B ~~ (f"B) -> z ~~ (f"B)))
67	66	com12 13	. . . . . . . . . . . . . . 15 |- (B ~~ (f"B) -> (z ~~ B -> z ~~ (f"B)))
68	55, 64, 67	3syl 21	. . . . . . . . . . . . . 14 |- ((f:A-1-1-onto->z /\ B (. A) -> (z ~~ B -> z ~~ (f"B)))
69	68	adantl 305	. . . . . . . . . . . . 13 |- ((z e. om /\ (f:A-1-1-onto->z /\ B (. A)) -> (z ~~ B -> z ~~ (f"B)))
70	52, 69	mtod 95	. . . . . . . . . . . 12 |- ((z e. om /\ (f:A-1-1-onto->z /\ B (. A)) -> -. z ~~ B)
71	70	exp32 294	. . . . . . . . . . 11 |- (z e. om -> (f:A-1-1-onto->z -> (B (. A -> -. z ~~ B)))
72	71	19.23adv 954	. . . . . . . . . 10 |- (z e. om -> (E.f f:A-1-1-onto->z -> (B (. A -> -. z ~~ B)))
73		visset 1350	. . . . . . . . . . 11 |- z e. V
74	73	bren 3282	. . . . . . . . . 10 |- (A ~~ z <-> E.f f:A-1-1-onto->z)
75	72, 74	syl5ib 181	. . . . . . . . 9 |- (z e. om -> (A ~~ z -> (B (. A -> -. z ~~ B)))
76	75	imp31 280	. . . . . . . 8 |- (((z e. om /\ A ~~ z) /\ B (. A) -> -. z ~~ B)
77		entrt 3319	. . . . . . . . . . . 12 |- ((B ~~ A /\ A ~~ z) -> B ~~ z)
78	77	exp 291	. . . . . . . . . . 11 |- (B ~~ A -> (A ~~ z -> B ~~ z))
79	73	ensym 3317	. . . . . . . . . . 11 |- (B ~~ z -> z ~~ B)
80	78, 79	syl6 23	. . . . . . . . . 10 |- (B ~~ A -> (A ~~ z -> z ~~ B))
81	80	com12 13	. . . . . . . . 9 |- (A ~~ z -> (B ~~ A -> z ~~ B))
82	81	ad2antlr 321	. . . . . . . 8 |- (((z e. om /\ A ~~ z) /\ B (. A) -> (B ~~ A -> z ~~ B))
83	76, 82	mtod 95	. . . . . . 7 |- (((z e. om /\ A ~~ z) /\ B (. A) -> -. B ~~ A)
84	7, 83	jca 236	. . . . . 6 |- (((z e. om /\ A ~~ z) /\ B (. A) -> (B ~<_ A /\ -. B ~~ A))
85		brsdom