Theorem php 4502

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 4497 through phplem4 4500, nneneq 4501, 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 3150	. . . . . . 7 ⊢ (A ∈ ω → (A = ∅ ⋁ ∃x ∈ ω A = suc x))
2	1	orcanai 689	. . . . . 6 ⊢ ((A ∈ ω ⋀ ¬ A = ∅) → ∃x ∈ ω A = suc x)
3		0ss 2298	. . . . . . . 8 ⊢ ∅ ⊆ B
4		sspsstr 2148	. . . . . . . 8 ⊢ ((∅ ⊆ B ⋀ B ⊂ A) → ∅ ⊂ A)
5	3, 4	mpan 694	. . . . . . 7 ⊢ (B ⊂ A → ∅ ⊂ A)
6		0pss 2305	. . . . . . . 8 ⊢ (∅ ⊂ A ↔ A ≠ ∅)
7		df-ne 1585	. . . . . . . 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 2133	. . . . . . . 8 ⊢ (A = suc x → (B ⊂ A ↔ B ⊂ suc x))
12		breq1 2618	. . . . . . . . 9 ⊢ (A = suc x → (A ≈ B ↔ suc x ≈ B))
13	12	negbid 610	. . . . . . . 8 ⊢ (A = suc x → (¬ A ≈ B ↔ ¬ suc x ≈ B))
14	11, 13	imbi12d 625	. . . . . . 7 ⊢ (A = suc x → ((B ⊂ A → ¬ A ≈ B) ↔ (B ⊂ suc x → ¬ suc x ≈ B)))
15		pssnel 2328	. . . . . . . . . 10 ⊢ (B ⊂ suc x → ∃y(y ∈ suc x ⋀ ¬ y ∈ B))
16		domentr 4411	. . . . . . . . . . . . . . 15 ⊢ ((B ≼ (suc x ∖ {y}) ⋀ (suc x ∖ {y}) ≈ x) → B ≼ x)
17		disjsn 2438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((B ∩ {y}) = ∅ ↔ ¬ y ∈ B)
18		disj3 2311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((B ∩ {y}) = ∅ ↔ B = (B ∖ {y}))
19	17, 18	bitr3 175	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ y ∈ B ↔ B = (B ∖ {y}))
20		sseq1 2079	. . . . . . . . . . . . . . . . . . . 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 2169	. . . . . . . . . . . . . . . . . . 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 1810	. . . . . . . . . . . . . . . . . . . . 21 ⊢ x ∈ V
25	24	sucex 3046	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc x ∈ V
26		difss 2164	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc x ∖ {y}) ⊆ suc x
27	25, 26	ssexi 2716	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc x ∖ {y}) ∈ V
28		ssdom2g 4399	. . . . . . . . . . . . . . . . . . 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 2140	. . . . . . . . . . . . . . . . 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 1810	. . . . . . . . . . . . . . . . 17 ⊢ y ∈ V
35	24, 34	phplem3 4499	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ ω ⋀ y ∈ suc x) → x ≈ (suc x ∖ {y}))
36	27	ensym 4402	. . . . . . . . . . . . . . . 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 1294	. . . . . . . . . 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 4410	. . . . . . . . . . . . 13 ⊢ ((suc x ≈ B ⋀ B ≼ x) → suc x ≼ x)
45		sssucid 3043	. . . . . . . . . . . . . 14 ⊢ x ⊆ suc x
46		ssdom2g 4399	. . . . . . . . . . . . . 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 4446	. . . . . . . . . . . 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 3143	. . . . . . . . . . . . 13 ⊢ (x ∈ ω ↔ suc x ∈ ω)
53		nnord 3136	. . . . . . . . . . . . 13 ⊢ (suc x ∈ ω → Ord suc x)
54	52, 53	sylbi 199	. . . . . . . . . . . 12 ⊢ (x ∈ ω → Ord suc x)
55	24	sucid 3047	. . . . . . . . . . . . 13 ⊢ x ∈ suc x
56		nordeq 2963	. . . . . . . . . . . . 13 ⊢ ((Ord suc x ⋀ x ∈ suc x) → suc x ≠ x)
57	55, 56	mpan2 695	. . . . . . . . . . . 12 ⊢ (Ord suc x → suc x ≠ x)
58	54, 57	syl 10	. . . . . . . . . . 11 ⊢ (x ∈ ω → suc x ≠ x)
59		nneneq 4501	. . . . . . . . . . . . . 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 1598	. . . . . . . . . . 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 1741	. . . . 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)

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223   = wceq 955   ∈ wcel 957  ∃wex 979   ≠ wne 1583  ∃wrex 1644  Vcvv 1808   ∖ cdif 2041   ∩ cin 2043   ⊆ wss 2044   ⊂ wpss 2045  ∅c0 2277  {csn 2406   class class class wbr 2615  Ord word 2943  suc csuc 2946  ωcom 3127   ≈ cen 4357   ≼ cdom 4358

This theorem is referenced by:  php2 4503  php3 4504

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-rep 2689  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-pr 2775  ax-un 2862

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-ral 1647  df-rex 1648  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-pss 2052  df-nul 2278  df-if 2359  df-pw 2399  df-sn 2409  df-pr 2410  df-tp 2412  df-op 2413  df-uni 2500  df-br 2616  df-opab 2663  df-tr 2677  df-eprel 2828  df-id 2831  df-po 2836  df-so 2846  df-fr 2913  df-we 2930  df-ord 2947  df-on 2948  df-lim 2949  df-suc 2950  df-om 3128  df-xp 3180  df-rel 3181  df-cnv 3182  df-co 3183  df-dm 3184  df-rn 3185  df-res 3186  df-ima 3187  df-fun 3188  df-fn 3189  df-f 3190  df-f1 3191  df-fo 3192  df-f1o 3193  df-fv 3194  df-er 4254  df-en 4360  df-dom 4361

Copyright terms: Public domain