php - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem php 4493

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 4488 through phplem4 4491, nneneq 4492, and this final piece of the proof.

**Assertion**
Ref	Expression
php	⊢ ((A ∈ ω ⋀ B ⊂ A) → ¬ A ≈ B)

**Proof of Theorem php**
Step	Hyp	Ref	Expression
1		nn0suc 3144	. . . . . . 7 ⊢ (A ∈ ω → (A = ∅ ⋁ ∃x ∈ ω A = suc x))
2	1	orcanai 688	. . . . . 6 ⊢ ((A ∈ ω ⋀ ¬ A = ∅) → ∃x ∈ ω A = suc x)
3		0ss 2291	. . . . . . . 8 ⊢ ∅ ⊆ B
4		sspsstr 2141	. . . . . . . 8 ⊢ ((∅ ⊆ B ⋀ B ⊂ A) → ∅ ⊂ A)
5	3, 4	mpan 693	. . . . . . 7 ⊢ (B ⊂ A → ∅ ⊂ A)
6		0pss 2298	. . . . . . . 8 ⊢ (∅ ⊂ A ↔ A ≠ ∅)
7		df-ne 1579	. . . . . . . 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 ∈ ω ⋀ B ⊂ A) → ∃x ∈ ω A = suc x)
11		psseq2 2126	. . . . . . . 8 ⊢ (A = suc x → (B ⊂ A ↔ B ⊂ suc x))
12		breq1 2612	. . . . . . . . 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 2321	. . . . . . . . . 10 ⊢ (B ⊂ suc x → ∃y(y ∈ suc x ⋀ ¬ y ∈ B))
16		domentr 4402	. . . . . . . . . . . . . . 15 ⊢ ((B ≼ (suc x ∖ {y}) ⋀ (suc x ∖ {y}) ≈ x) → B ≼ x)
17		disjsn 2431	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((B ∩ {y}) = ∅ ↔ ¬ y ∈ B)
18		disj3 2304	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((B ∩ {y}) = ∅ ↔ B = (B ∖ {y}))
19	17, 18	bitr3 175	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ y ∈ B ↔ B = (B ∖ {y}))
20		sseq1 2072	. . . . . . . . . . . . . . . . . . . 20 ⊢ (B = (B ∖ {y}) → (B ⊆ (suc x ∖ {y}) ↔ (B ∖ {y}) ⊆ (suc x ∖ {y})))
21	19, 20	sylbi 199	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ y ∈ B → (B ⊆ (suc x ∖ {y}) ↔ (B ∖ {y}) ⊆ (suc x ∖ {y})))
22		ssdif 2162	. . . . . . . . . . . . . . . . . . 19 ⊢ (B ⊆ suc x → (B ∖ {y}) ⊆ (suc x ∖ {y}))
23	21, 22	syl5bir 210	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ y ∈ B → (B ⊆ suc x → B ⊆ (suc x ∖ {y})))
24		visset 1804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ x ∈ V
25	24	sucex 3040	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc x ∈ V
26		difss 2157	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc x ∖ {y}) ⊆ suc x
27	25, 26	ssexi 2710	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc x ∖ {y}) ∈ V
28		ssdom2g 4390	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc x ∖ {y}) ∈ 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 ∈ B → (B ⊆ suc x → B ≼ (suc x ∖ {y})))
31		pssss 2133	. . . . . . . . . . . . . . . . 17 ⊢ (B ⊂ suc x → B ⊆ suc x)
32	30, 31	syl5 21	. . . . . . . . . . . . . . . 16 ⊢ (¬ y ∈ B → (B ⊂ suc x → B ≼ (suc x ∖ {y})))
33	32	imp 350	. . . . . . . . . . . . . . 15 ⊢ ((¬ y ∈ B ⋀ B ⊂ suc x) → B ≼ (suc x ∖ {y}))
34		visset 1804	. . . . . . . . . . . . . . . . 17 ⊢ y ∈ V
35	24, 34	phplem3 4490	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ ω ⋀ y ∈ suc x) → x ≈ (suc x ∖ {y}))
36	27	ensym 4393	. . . . . . . . . . . . . . . 16 ⊢ (x ≈ (suc x ∖ {y}) → (suc x ∖ {y}) ≈ x)
37	35, 36	syl 10	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ ω ⋀ y ∈ suc x) → (suc x ∖ {y}) ≈ x)
38	16, 33, 37	syl2an 454	. . . . . . . . . . . . . 14 ⊢ (((¬ y ∈ B ⋀ B ⊂ suc x) ⋀ (x ∈ ω ⋀ y ∈ suc x)) → B ≼ x)
39	38	exp43 384	. . . . . . . . . . . . 13 ⊢ (¬ y ∈ B → (B ⊂ suc x → (x ∈ ω → (y ∈ suc x → B ≼ x))))
40	39	com4r 41	. . . . . . . . . . . 12 ⊢ (y ∈ suc x → (¬ y ∈ B → (B ⊂ suc x → (x ∈ ω → B ≼ x))))
41	40	imp 350	. . . . . . . . . . 11 ⊢ ((y ∈ suc x ⋀ ¬ y ∈ B) → (B ⊂ suc x → (x ∈ ω → B ≼ x)))
42	41	19.23aiv 1290	. . . . . . . . . 10 ⊢ (∃y(y ∈ suc x ⋀ ¬ y ∈ B) → (B ⊂ suc x → (x ∈ ω → B ≼ x)))
43	15, 42	mpcom 49	. . . . . . . . 9 ⊢ (B ⊂ suc x → (x ∈ ω → B ≼ x))
44		endomtr 4401	. . . . . . . . . . . . 13 ⊢ ((suc x ≈ B ⋀ B ≼ x) → suc x ≼ x)
45		sssucid 3037	. . . . . . . . . . . . . 14 ⊢ x ⊆ suc x
46		ssdom2g 4390	. . . . . . . . . . . . . 14 ⊢ (suc x ∈ 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 4437	. . . . . . . . . . . 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 3137	. . . . . . . . . . . . 13 ⊢ (x ∈ ω ↔ suc x ∈ ω)
53		nnord 3130	. . . . . . . . . . . . 13 ⊢ (suc x ∈ ω → Ord suc x)
54	52, 53	sylbi 199	. . . . . . . . . . . 12 ⊢ (x ∈ ω → Ord suc x)
55	24	sucid 3041	. . . . . . . . . . . . 13 ⊢ x ∈ suc x
56		nordeq 2957	. . . . . . . . . . . . 13 ⊢ ((Ord suc x ⋀ x ∈ suc x) → suc x ≠ x)
57	55, 56	mpan2 694	. . . . . . . . . . . 12 ⊢ (Ord suc x → suc x ≠ x)
58	54, 57	syl 10	. . . . . . . . . . 11 ⊢ (x ∈ ω → suc x ≠ x)
59		nneneq 4492	. . . . . . . . . . . . . 14 ⊢ ((suc x ∈ ω ⋀ x ∈ ω) → (suc x ≈ x ↔ suc x = x))
60	59, 52	sylanb 449	. . . . . . . . . . . . 13 ⊢ ((x ∈ ω ⋀ x ∈ ω) → (suc x ≈ x ↔ suc x = x))
61	60	anidms 434	. . . . . . . . . . . 12 ⊢ (x ∈ ω → (suc x ≈ x ↔ suc x = x))
62	61	necon3bbid 1592	. . . . . . . . . . 11 ⊢ (x ∈ ω → (¬ suc x ≈ x ↔ suc x ≠ x))
63	58, 62	mpbird 196	. . . . . . . . . 10 ⊢ (x ∈ ω → ¬ suc x ≈ x)
64	51, 63	nsyli 121	. . . . . . . . 9 ⊢ (B ≼ x → (x ∈ ω → ¬ suc x ≈ B))
65	43, 64	syli 54	. . . . . . . 8 ⊢ (B ⊂ suc x → (x ∈ ω → ¬ suc x ≈ B))
66	65	com12 11	. . . . . . 7 ⊢ (x ∈ ω → (B ⊂ suc x → ¬ suc x ≈ B))
67	14, 66	syl5cbir 211	. . . . . 6 ⊢ (x ∈ ω → (A = suc x → (B ⊂ A → ¬ A ≈ B)))
68	67	r19.23aiv 1735	. . . . 5 ⊢ (∃x ∈ ω A = suc x → (B ⊂ A → ¬ A ≈ B))
69	10, 68	syl 10	. . . 4 ⊢ ((A ∈ ω ⋀ B ⊂ A) → (B ⊂ A → ¬ A ≈ B))
70	69	ex 373	. . 3 ⊢ (A ∈ ω → (B ⊂ A → (B ⊂ A → ¬ A ≈ B)))
71	70	pm2.43d 65	. 2 ⊢ (A ∈ ω → (B ⊂ A → ¬ A ≈ B))
72	71	imp 350	1 ⊢ ((A ∈ ω ⋀ B ⊂ A) → ¬ A ≈ B)

Colors of variables: wff set class

Syntax hints: ¬ wn 2 → wi 3 ↔ wb 146 ⋀ wa 223 = wceq 953 ∈ wcel 955 ∃wex 977 ≠ wne 1577 ∃wrex 1638 Vcvv 1802 ∖ cdif 2034 ∩ cin 2036 ⊆ wss 2037 ⊂ wpss 2038 ∅c0 2270 {csn 2399 class class class wbr 2609 Ord word 2937 suc csuc 2940 ωcom 3121 ≈ cen 4348 ≼ cdom 4349

This theorem is referenced by: php2 4494 php3 4495

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-9 962 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-rep 2683 ax-sep 2693 ax-nul 2700 ax-pow 2732 ax-pr 2769 ax-un 2857

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 774 df-3an 775 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-ral 1641 df-rex 1642 df-v 1803 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-pss 2045 df-nul 2271 df-if 2352 df-pw 2392 df-sn 2402 df-pr 2403 df-tp 2405 df-op 2406 df-uni 2494 df-br 2610 df-opab 2657 df-tr 2671 df-eprel 2821 df-id 2824 df-po 2831 df-so 2841 df-fr 2907 df-we 2924 df-ord 2941 df-on 2942 df-lim 2943 df-suc 2944 df-om 3122 df-xp 3174 df-rel 3175 df-cnv 3176 df-co 3177 df-dm 3178 df-rn 3179 df-res 3180 df-ima 3181 df-fun 3182 df-fn 3183 df-f 3184 df-f1 3185 df-fo 3186 df-f1o 3187 df-fv 3188 df-er 4245 df-en 4351 df-dom 4352