Theorem php 4445

Description: Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. Theorem (Pigeonhole Principle) of [Enderton] p. 134. The theorem is so-called because you can't put n + 1 pigeons into n holes (if each hole holds only one pigeon). The proof consists of lemmas phplem1 4440 through phplem4 4443, nneneq 4444, and this final piece of the proof.

Assertion

Ref	Expression
php	|- ((A e. om /\ B (. A) -> -. A ~~ B)

Proof of Theorem php

Step	Hyp	Ref	Expression
1		nn0suc 3117	. . . . . . 7 |- (A e. om -> (A = (/) \/ E.x e. om A = suc x))
2	1	orcanai 687	. . . . . 6 |- ((A e. om /\ -. A = (/)) -> E.x e. om A = suc x)
3		0ss 2272	. . . . . . . 8 |- (/) (_ B
4		sspsstr 2122	. . . . . . . 8 |- (((/) (_ B /\ B (. A) -> (/) (. A)
5	3, 4	mpan 692	. . . . . . 7 |- (B (. A -> (/) (. A)
6		0pss 2279	. . . . . . . 8 |- ((/) (. A <-> A =/= (/))
7		df-ne 1563	. . . . . . . 8 |- (A =/= (/) <-> -. A = (/))
8	6, 7	bitr 173	. . . . . . 7 |- ((/) (. A <-> -. A = (/))
9	5, 8	sylib 198	. . . . . 6 |- (B (. A -> -. A = (/))
10	2, 9	sylan2 451	. . . . 5 |- ((A e. om /\ B (. A) -> E.x e. om A = suc x)
11		psseq2 2107	. . . . . . . 8 |- (A = suc x -> (B (. A <-> B (. suc x))
12		breq1 2590	. . . . . . . . 9 |- (A = suc x -> (A ~~ B <-> suc x ~~ B))
13	12	negbid 609	. . . . . . . 8 |- (A = suc x -> (-. A ~~ B <-> -. suc x ~~ B))
14	11, 13	imbi12d 624	. . . . . . 7 |- (A = suc x -> ((B (. A -> -. A ~~ B) <-> (B (. suc x -> -. suc x ~~ B)))
15		pssnel 2302	. . . . . . . . . 10 |- (B (. suc x -> E.y(y e. suc x /\ -. y e. B))
16		domentr 4356	. . . . . . . . . . . . . . 15 |- ((B ~<_ (suc x \ {y}) /\ (suc x \ {y}) ~~ x) -> B ~<_ x)
17		disjsn 2412	. . . . . . . . . . . . . . . . . . . . 21 |- ((B i^i {y}) = (/) <-> -. y e. B)
18		disj3 2285	. . . . . . . . . . . . . . . . . . . . 21 |- ((B i^i {y}) = (/) <-> B = (B \ {y}))
19	17, 18	bitr3 175	. . . . . . . . . . . . . . . . . . . 20 |- (-. y e. B <-> B = (B \ {y}))
20		sseq1 2053	. . . . . . . . . . . . . . . . . . . 20 |- (B = (B \ {y}) -> (B (_ (suc x \ {y}) <-> (B \ {y}) (_ (suc x \ {y})))
21	19, 20	sylbi 199	. . . . . . . . . . . . . . . . . . 19 |- (-. y e. B -> (B (_ (suc x \ {y}) <-> (B \ {y}) (_ (suc x \ {y})))
22		ssdif 2143	. . . . . . . . . . . . . . . . . . 19 |- (B (_ suc x -> (B \ {y}) (_ (suc x \ {y}))
23	21, 22	syl5bir 210	. . . . . . . . . . . . . . . . . 18 |- (-. y e. B -> (B (_ suc x -> B (_ (suc x \ {y})))
24		visset 1788	. . . . . . . . . . . . . . . . . . . . 21 |- x e. V
25	24	sucex 3013	. . . . . . . . . . . . . . . . . . . 20 |- suc x e. V
26		difss 2138	. . . . . . . . . . . . . . . . . . . 20 |- (suc x \ {y}) (_ suc x
27	25, 26	ssexi 2688	. . . . . . . . . . . . . . . . . . 19 |- (suc x \ {y}) e. V
28		ssdom2g 4344	. . . . . . . . . . . . . . . . . . 19 |- ((suc x \ {y}) e. V -> (B (_ (suc x \ {y}) -> B ~<_ (suc x \ {y})))
29	27, 28	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- (B (_ (suc x \ {y}) -> B ~<_ (suc x \ {y}))
30	23, 29	syl6 22	. . . . . . . . . . . . . . . . 17 |- (-. y e. B -> (B (_ suc x -> B ~<_ (suc x \ {y})))
31		pssss 2114	. . . . . . . . . . . . . . . . 17 |- (B (. suc x -> B (_ suc x)
32	30, 31	syl5 21	. . . . . . . . . . . . . . . 16 |- (-. y e. B -> (B (. suc x -> B ~<_ (suc x \ {y})))
33	32	imp 350	. . . . . . . . . . . . . . 15 |- ((-. y e. B /\ B (. suc x) -> B ~<_ (suc x \ {y}))
34		visset 1788	. . . . . . . . . . . . . . . . 17 |- y e. V
35	24, 34	phplem3 4442	. . . . . . . . . . . . . . . 16 |- ((x e. om /\ y e. suc x) -> x ~~ (suc x \ {y}))
36	27	ensym 4347	. . . . . . . . . . . . . . . 16 |- (x ~~ (suc x \ {y}) -> (suc x \ {y}) ~~ x)
37	35, 36	syl 10	. . . . . . . . . . . . . . 15 |- ((x e. om /\ y e. suc x) -> (suc x \ {y}) ~~ x)
38	16, 33, 37	syl2an 454	. . . . . . . . . . . . . 14 |- (((-. y e. B /\ B (. suc x) /\ (x e. om /\ y e. suc x)) -> B ~<_ x)
39	38	exp43 384	. . . . . . . . . . . . 13 |- (-. y e. B -> (B (. suc x -> (x e. om -> (y e. suc x -> B ~<_ x))))
40	39	com4r 41	. . . . . . . . . . . 12 |- (y e. suc x -> (-. y e. B -> (B (. suc x -> (x e. om -> B ~<_ x))))
41	40	imp 350	. . . . . . . . . . 11 |- ((y e. suc x /\ -. y e. B) -> (B (. suc x -> (x e. om -> B ~<_ x)))
42	41	19.23aiv 1277	. . . . . . . . . 10 |- (E.y(y e. suc x /\ -. y e. B) -> (B (. suc x -> (x e. om -> B ~<_ x)))
43	15, 42	mpcom 49	. . . . . . . . 9 |- (B (. suc x -> (x e. om -> B ~<_ x))
44		endomtr 4355	. . . . . . . . . . . . 13 |- ((suc x ~~ B /\ B ~<_ x) -> suc x ~<_ x)
45		sssucid 3010	. . . . . . . . . . . . . 14 |- x (_ suc x
46		ssdom2g 4344	. . . . . . . . . . . . . 14 |- (suc x e. V -> (x (_ suc x -> x ~<_ suc x))
47	25, 45, 46	mp2 43	. . . . . . . . . . . . 13 |- x ~<_ suc x
48	44, 47	jctir 293	. . . . . . . . . . . 12 |- ((suc x ~~ B /\ B ~<_ x) -> (suc x ~<_ x /\ x ~<_ suc x))
49		sbth 4391	. . . . . . . . . . . 12 |- ((suc x ~<_ x /\ x ~<_ suc x) -> suc x ~~ x)
50	48, 49	syl 10	. . . . . . . . . . 11 |- ((suc x ~~ B /\ B ~<_ x) -> suc x ~~ x)
51	50	expcom 374	. . . . . . . . . 10 |- (B ~<_ x -> (suc x ~~ B -> suc x ~~ x))
52		peano2b 3110	. . . . . . . . . . . . 13 |- (x e. om <-> suc x e. om)
53		nnord 3103	. . . . . . . . . . . . 13 |- (suc x e. om -> Ord suc x)
54	52, 53	sylbi 199	. . . . . . . . . . . 12 |- (x e. om -> Ord suc x)
55	24	sucid 3014	. . . . . . . . . . . . 13 |- x e. suc x
56		nordeq 2930	. . . . . . . . . . . . 13 |- ((Ord suc x /\ x e. suc x) -> suc x =/= x)
57	55, 56	mpan2 693	. . . . . . . . . . . 12 |- (Ord suc x -> suc x =/= x)
58	54, 57	syl 10	. . . . . . . . . . 11 |- (x e. om -> suc x =/= x)
59		nneneq 4444	. . . . . . . . . . . . . 14 |- ((suc x e. om /\ x e. om) -> (suc x ~~ x <-> suc x = x))
60	59, 52	sylanb 449	. . . . . . . . . . . . 13 |- ((x e. om /\ x e. om) -> (suc x ~~ x <-> suc x = x))
61	60	anidms 434	. . . . . . . . . . . 12 |- (x e. om -> (suc x ~~ x <-> suc x = x))
62	61	necon3bbid 1576	. . . . . . . . . . 11 |- (x e. om -> (-. suc x ~~ x <-> suc x =/= x))
63	58, 62	mpbird 196	. . . . . . . . . 10 |- (x e. om -> -. suc x ~~ x)
64	51, 63	nsyli 121	. . . . . . . . 9 |- (B ~<_ x -> (x e. om -> -. suc x ~~ B))
65	43, 64	syli 54	. . . . . . . 8 |- (B (. suc x -> (x e. om -> -. suc x ~~ B))
66	65	com12 11	. . . . . . 7 |- (x e. om -> (B (. suc x -> -. suc x ~~ B))
67	14, 66	syl5cbir 211	. . . . . 6 |- (x e. om -> (A = suc x -> (B (. A -> -. A ~~ B)))
68	67	r19.23aiv 1719	. . . . 5 |- (E.x e. om A = suc x -> (B (. A -> -. A ~~ B))
69	10, 68	syl 10	. . . 4 |- ((A e. om /\ B (. A) -> (B (. A -> -. A ~~ B))
70	69	ex 373	. . 3 |- (A e. om -> (B (. A -> (B (. A -> -. A ~~ B)))
71	70	pm2.43d 65	. 2 |- (A e. om -> (B (. A -> -. A ~~ B))
72	71	imp 350	1 |- ((A e. om /\ B (. A) -> -. A ~~ B)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  E.wex 956   = wceq 1099   e. wcel 1105   =/= wne 1561  E.wrex 1622  Vcvv 1786   \ cdif 2015   i^i cin 2017   (_ wss 2018   (. wpss 2019  (/)c0 2251  {csn 2380   class class class wbr 2587  Ord word 2910  suc csuc 2913  omcom 3094   ~~ cen 4302   ~<_ cdom 4303

This theorem is referenced by:  php2 4446  php3 4447

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-pss 2026  df-nul 2252  df-if 2333  df-pw 2373  df-sn 2383  df-pr 2384  df-tp 2386  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-tr 2649  df-eprel 2794  df-id 2797  df-po 2804  df-so 2814  df-fr 2880  df-we 2897  df-ord 2914  df-on 2915  df-lim 2916  df-suc 2917  df-om 3095  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-f 3157  df-f1 3158  df-fo 3159  df-f1o 3160  df-fv 3161  df-er 4199  df-en 4305  df-dom 4306

Copyright terms: Public domain