Theorem php3 4501

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:   x,A

Proof of Theorem php3

Step	Hyp	Ref	Expression
1		ssdom2g 4396	. . . . . . . . . 10 |- (A e. V -> (B (_ A -> B ~<_ A))
2	1	imp 350	. . . . . . . . 9 |- ((A e. V /\ B (_ A) -> B ~<_ A)
3		relen 4360	. . . . . . . . . 10 |- Rel ~~
4	3	brrelexi 3203	. . . . . . . . 9 |- (A ~~ z -> A e. V)
5		pssss 2139	. . . . . . . . 9 |- (B (. A -> B (_ A)
6	2, 4, 5	syl2an 454	. . . . . . . 8 |- ((A ~~ z /\ B (. A) -> B ~<_ A)
7	6	adantll 392	. . . . . . 7 |- (((z e. om /\ A ~~ z) /\ B (. A) -> B ~<_ A)
8		php 4499	. . . . . . . . . . . . . 14 |- ((z e. om /\ (f"B) (. z) -> -. z ~~ (f"B))
9		imass2 3425	. . . . . . . . . . . . . . . . . . 19 |- (B (_ A -> (f"B) (_ (f"A))
10	5, 9	syl 10	. . . . . . . . . . . . . . . . . 18 |- (B (. A -> (f"B) (_ (f"A))
11	10	adantl 388	. . . . . . . . . . . . . . . . 17 |- ((f:A-1-1-onto->z /\ B (. A) -> (f"B) (_ (f"A))
12		funfvima2 3844	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Fun f /\ (A \ B) (_ dom f) -> (y e. (A \ B) -> (f` y) e. (f"(A \ B))))
13		f1ofun 3682	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:A-1-1-onto->z -> Fun f)
14		difss 2163	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A \ B) (_ A
15		f1ofn 3681	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:A-1-1-onto->z -> f Fn A)
16		fndm 3579	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f Fn A -> dom f = A)
17		sseq2 2079	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (dom f = A -> ((A \ B) (_ dom f <-> (A \ B) (_ A))
18	15, 16, 17	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:A-1-1-onto->z -> ((A \ B) (_ dom f <-> (A \ B) (_ A))
19	14, 18	mpbiri 194	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:A-1-1-onto->z -> (A \ B) (_ dom f)
20	12, 13, 19	sylanc 471	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:A-1-1-onto->z -> (y e. (A \ B) -> (f` y) e. (f"(A \ B))))
21		f1o3 3685	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f:A-1-1-onto->z <-> (f:A-onto->z /\ Fun `'f))
22	21	pm3.27bi 326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f:A-1-1-onto->z -> Fun `'f)
23		imadif 3566	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (Fun `'f -> (f"(A \ B)) = ((f"A) \ (f"B)))
24	22, 23	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (f:A-1-1-onto->z -> (f"(A \ B)) = ((f"A) \ (f"B)))
25	24	eleq2d 1538	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f:A-1-1-onto->z -> ((f` y) e. (f"(A \ B)) <-> (f` y) e. ((f"A) \ (f"B))))
26	20, 25	sylibd 202	. . . . . . . . . . . . . . . . . . . . . . 23 |- (f:A-1-1-onto->z -> (y e. (A \ B) -> (f` y) e. ((f"A) \ (f"B))))
27		n0i 2281	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f` y) e. ((f"A) \ (f"B)) -> -. ((f"A) \ (f"B)) = (/))
28	26, 27	syl6 22	. . . . . . . . . . . . . . . . . . . . . 22 |- (f:A-1-1-onto->z -> (y e. (A \ B) -> -. ((f"A) \ (f"B)) = (/)))
29		eldif 2053	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. (A \ B) <-> (y e. A /\ -. y e. B))
30	28, 29	syl5ibr 207	. . . . . . . . . . . . . . . . . . . . 21 |- (f:A-1-1-onto->z -> ((y e. A /\ -. y e. B) -> -. ((f"A) \ (f"B)) = (/)))
31	30	19.23adv 1212	. . . . . . . . . . . . . . . . . . . 20 |- (f:A-1-1-onto->z -> (E.y(y e. A /\ -. y e. B) -> -. ((f"A) \ (f"B)) = (/)))
32	31	imp 350	. . . . . . . . . . . . . . . . . . 19 |- ((f:A-1-1-onto->z /\ E.y(y e. A /\ -. y e. B)) -> -. ((f"A) \ (f"B)) = (/))
33		pssnel 2327	. . . . . . . . . . . . . . . . . . 19 |- (B (. A -> E.y(y e. A /\ -. y e. B))
34	32, 33	sylan2 451	. . . . . . . . . . . . . . . . . 18 |- ((f:A-1-1-onto->z /\ B (. A) -> -. ((f"A) \ (f"B)) = (/))
35		ssdif0 2323	. . . . . . . . . . . . . . . . . . 19 |- ((f"A) (_ (f"B) <-> ((f"A) \ (f"B)) = (/))
36	35	negbii 187	. . . . . . . . . . . . . . . . . 18 |- (-. (f"A) (_ (f"B) <-> -. ((f"A) \ (f"B)) = (/))
37	34, 36	sylibr 200	. . . . . . . . . . . . . . . . 17 |- ((f:A-1-1-onto->z /\ B (. A) -> -. (f"A) (_ (f"B))
38	11, 37	jca 288	. . . . . . . . . . . . . . . 16 |- ((f:A-1-1-onto->z /\ B (. A) -> ((f"B) (_ (f"A) /\ -. (f"A) (_ (f"B)))
39		dfpss3 2130	. . . . . . . . . . . . . . . 16 |- ((f"B) (. (f"A) <-> ((f"B) (_ (f"A) /\ -. (f"A) (_ (f"B)))
40	38, 39	sylibr 200	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->z /\ B (. A) -> (f"B) (. (f"A))
41		imadmrn 3406	. . . . . . . . . . . . . . . . . . 19 |- (f"dom f) = ran f
42	41	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (f:A-1-1-onto->z -> (f"dom f) = ran f)
43		imaeq2 3394	. . . . . . . . . . . . . . . . . . 19 |- (dom f = A -> (f"dom f) = (f"A))
44	15, 16, 43	3syl 20	. . . . . . . . . . . . . . . . . 18 |- (f:A-1-1-onto->z -> (f"dom f) = (f"A))
45		f1ofo 3686	. . . . . . . . . . . . . . . . . . 19 |- (f:A-1-1-onto->z -> f:A-onto->z)
46		forn 3665	. . . . . . . . . . . . . . . . . . 19 |- (f:A-onto->z -> ran f = z)
47	45, 46	syl 10	. . . . . . . . . . . . . . . . . 18 |- (f:A-1-1-onto->z -> ran f = z)
48	42, 44, 47	3eqtr3d 1512	. . . . . . . . . . . . . . . . 17 |- (f:A-1-1-onto->z -> (f"A) = z)
49	48	psseq2d 2137	. . . . . . . . . . . . . . . 16 |- (f:A-1-1-onto->z -> ((f"B) (. (f"A) <-> (f"B) (. z))
50	49	adantr 389	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->z /\ B (. A) -> ((f"B) (. (f"A) <-> (f"B) (. z))
51	40, 50	mpbid 195	. . . . . . . . . . . . . 14 |- ((f:A-1-1-onto->z /\ B (. A) -> (f"B) (. z)
52	8, 51	sylan2 451	. . . . . . . . . . . . 13 |- ((z e. om /\ (f:A-1-1-onto->z /\ B (. A)) -> -. z ~~ (f"B))
53		f1ores 3694	. . . . . . . . . . . . . . . 16 |- ((f:A-1-1->z /\ B (_ A) -> (f |` B):B-1-1-onto->(f"B))
54		f1of1 3679	. . . . . . . . . . . . . . . 16 |- (f:A-1-1-onto->z -> f:A-1-1->z)
55	53, 54, 5	syl2an 454	. . . . . . . . . . . . . . 15 |- ((f:A-1-1-onto->z /\ B (. A) -> (f |` B):B-1-1-onto->(f"B))
56		visset 1809	. . . . . . . . . . . . . . . . . 18 |- f e. V
57		resexg 3386	. . . . . . . . . . . . . . . . . 18 |- (f e. V -> (f |` B) e. V)
58	56, 57	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (f |` B) e. V
59		f1oeq1 3675	. . . . . . . . . . . . . . . . 17 |- (y = (f |` B) -> (y:B-1-1-onto->(f"B) <-> (f |` B):B-1-1-onto->(f"B)))
60	58, 59	cla4ev 1865	. . . . . . . . . . . . . . . 16 |- ((f |` B):B-1-1-onto->(f"B) -> E.y y:B-1-1-onto->(f"B))
61		imaexg 3408	. . . . . . . . . . . . . . . . . 18 |- (f e. V -> (f"B) e. V)
62	56, 61	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- (f"B) e. V
63	62	bren 4365	. . . . . . . . . . . . . . . 16 |- (B ~~ (f"B) <-> E.y y:B-1-1-onto->(f"B))
64	60, 63	sylibr 200	. . . . . . . . . . . . . . 15 |- ((f |` B):B-1-1-onto->(f"B) -> B ~~ (f"B))
65		entrt 4401	. . . . . . . . . . . . . . . 16 |- ((z ~~ B /\ B ~~ (f"B)) -> z ~~ (f"B))
66	65	expcom 374	. . . . . . . . . . . . . . 15 |- (B ~~ (f"B) -> (z ~~ B -> z ~~ (f"B)))
67	55, 64, 66	3syl 20	. . . . . . . . . . . . . 14 |- ((f:A-1-1-onto->z /\ B (. A) -> (z ~~ B -> z ~~ (f"B)))
68	67	adantl 388	. . . . . . . . . . . . 13 |- ((z e. om /\ (f:A-1-1-onto->z /\ B (. A)) -> (z ~~ B -> z ~~ (f"B)))
69	52, 68	mtod 108	. . . . . . . . . . . 12 |- ((z e. om /\ (f:A-1-1-onto->z /\ B (. A)) -> -. z ~~ B)
70	69	exp32 377	. . . . . . . . . . 11 |- (z e. om -> (f:A-1-1-onto->z -> (B (. A -> -. z ~~ B)))
71	70	19.23adv 1212	. . . . . . . . . 10 |- (z e. om -> (E.f f:A-1-1-onto->z -> (B (. A -> -. z ~~ B)))
72		visset 1809	. . . . . . . . . . 11 |- z e. V
73	72	bren 4365	. . . . . . . . . 10 |- (A ~~ z <-> E.f f:A-1-1-onto->z)
74	71, 73	syl5ib 206	. . . . . . . . 9 |- (z e. om -> (A ~~ z -> (B (. A -> -. z ~~ B)))
75	74	imp31 362	. . . . . . . 8 |- (((z e. om /\ A ~~ z) /\ B (. A) -> -. z ~~ B)
76		entrt 4401	. . . . . . . . . . 11 |- ((B ~~ A /\ A ~~ z) -> B ~~ z)
77	76	ex 373	. . . . . . . . . 10 |- (B ~~ A -> (A ~~ z -> B ~~ z))
78	72	ensym 4399	. . . . . . . . . 10 |- (B ~~ z -> z ~~ B)
79	77, 78	syl6com 53	. . . . . . . . 9 |- (A ~~ z -> (B ~~ A -> z ~~ B))
80	79	ad2antlr 405	. . . . . . . 8 |- (((z e. om /\ A ~~ z) /\ B (. A) -> (B ~~ A -> z ~~ B))
81	75, 80	mtod 108	. . . . . . 7 |- (((z e. om /\ A ~~ z