Theorem php 3409

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 3403 through phplem5 3407, nneneq 3408, 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 2395	. . . . . . 7 ⊢ (A ∈ ω → (A = ∅ ∨ ∃x ∈ ω A = suc x))
2	1	orcanai 515	. . . . . 6 ⊢ ((A ∈ ω ∧ ¬ A = ∅) → ∃x ∈ ω A = suc x)
3		0ss 1725	. . . . . . . 8 ⊢ ∅ ⊆ B
4		sspsstr 1575	. . . . . . . 8 ⊢ ((∅ ⊆ B ∧ B ⊂ A) → ∅ ⊂ A)
5	3, 4	mpan 518	. . . . . . 7 ⊢ (B ⊂ A → ∅ ⊂ A)
6		0pss 1730	. . . . . . 7 ⊢ (∅ ⊂ A ↔ ¬ A = ∅)
7	5, 6	sylib 173	. . . . . 6 ⊢ (B ⊂ A → ¬ A = ∅)
8	2, 7	sylan2 346	. . . . 5 ⊢ ((A ∈ ω ∧ B ⊂ A) → ∃x ∈ ω A = suc x)
9		psseq2 1560	. . . . . . . . 9 ⊢ (A = suc x → (B ⊂ A ↔ B ⊂ suc x))
10		breq1 2065	. . . . . . . . . 10 ⊢ (A = suc x → (A ≈ B ↔ suc x ≈ B))
11	10	negbid 463	. . . . . . . . 9 ⊢ (A = suc x → (¬ A ≈ B ↔ ¬ suc x ≈ B))
12	9, 11	imbi12d 474	. . . . . . . 8 ⊢ (A = suc x → ((B ⊂ A → ¬ A ≈ B) ↔ (B ⊂ suc x → ¬ suc x ≈ B)))
13		pssnel 1752	. . . . . . . . . . 11 ⊢ (B ⊂ suc x → ∃y(y ∈ suc x ∧ ¬ y ∈ B))
14		domentr 3326	. . . . . . . . . . . . . . . 16 ⊢ ((B ≼ (suc x ∖ {y}) ∧ (suc x ∖ {y}) ≈ x) → B ≼ x)
15		disjsn 1836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((B ∩ {y}) = ∅ ↔ ¬ y ∈ B)
16		disj3 1736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((B ∩ {y}) = ∅ ↔ B = (B ∖ {y}))
17	15, 16	bitr3 153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ y ∈ B ↔ B = (B ∖ {y}))
18		sseq1 1521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (B = (B ∖ {y}) → (B ⊆ (suc x ∖ {y}) ↔ (B ∖ {y}) ⊆ (suc x ∖ {y})))
19	17, 18	sylbi 174	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ y ∈ B → (B ⊆ (suc x ∖ {y}) ↔ (B ∖ {y}) ⊆ (suc x ∖ {y})))
20		ssdif 1600	. . . . . . . . . . . . . . . . . . . 20 ⊢ (B ⊆ suc x → (B ∖ {y}) ⊆ (suc x ∖ {y}))
21	19, 20	syl5bir 184	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ y ∈ B → (B ⊆ suc x → B ⊆ (suc x ∖ {y})))
22		visset 1350	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ x ∈ V
23	22	sucex 2303	. . . . . . . . . . . . . . . . . . . . 21 ⊢ suc x ∈ V
24		difss 1596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (suc x ∖ {y}) ⊆ suc x
25	23, 24	ssexi 1701	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc x ∖ {y}) ∈ V
26		ssdom2g 3312	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((suc x ∖ {y}) ∈ V → (B ⊆ (suc x ∖ {y}) → B ≼ (suc x ∖ {y})))
27	25, 26	ax-mp 6	. . . . . . . . . . . . . . . . . . 19 ⊢ (B ⊆ (suc x ∖ {y}) → B ≼ (suc x ∖ {y}))
28	21, 27	syl6 23	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ y ∈ B → (B ⊆ suc x → B ≼ (suc x ∖ {y})))
29		pssss 1567	. . . . . . . . . . . . . . . . . 18 ⊢ (B ⊂ suc x → B ⊆ suc x)
30	28, 29	syl5 22	. . . . . . . . . . . . . . . . 17 ⊢ (¬ y ∈ B → (B ⊂ suc x → B ≼ (suc x ∖ {y})))
31	30	imp 277	. . . . . . . . . . . . . . . 16 ⊢ ((¬ y ∈ B ∧ B ⊂ suc x) → B ≼ (suc x ∖ {y}))
32		visset 1350	. . . . . . . . . . . . . . . . . 18 ⊢ y ∈ V
33	22, 32	phplem4 3406	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ ω ∧ y ∈ suc x) → x ≈ (suc x ∖ {y}))
34	25	ensym 3317	. . . . . . . . . . . . . . . . 17 ⊢ (x ≈ (suc x ∖ {y}) → (suc x ∖ {y}) ≈ x)
35	33, 34	syl 12	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ ω ∧ y ∈ suc x) → (suc x ∖ {y}) ≈ x)
36	14, 31, 35	syl2an 349	. . . . . . . . . . . . . . 15 ⊢ (((¬ y ∈ B ∧ B ⊂ suc x) ∧ (x ∈ ω ∧ y ∈ suc x)) → B ≼ x)
37	36	exp43 301	. . . . . . . . . . . . . 14 ⊢ (¬ y ∈ B → (B ⊂ suc x → (x ∈ ω → (y ∈ suc x → B ≼ x))))
38	37	com4r 41	. . . . . . . . . . . . 13 ⊢ (y ∈ suc x → (¬ y ∈ B → (B ⊂ suc x → (x ∈ ω → B ≼ x))))
39	38	imp 277	. . . . . . . . . . . 12 ⊢ ((y ∈ suc x ∧ ¬ y ∈ B) → (B ⊂ suc x → (x ∈ ω → B ≼ x)))
40	39	19.23aiv 952	. . . . . . . . . . 11 ⊢ (∃y(y ∈ suc x ∧ ¬ y ∈ B) → (B ⊂ suc x → (x ∈ ω → B ≼ x)))
41	13, 40	mpcom 49	. . . . . . . . . 10 ⊢ (B ⊂ suc x → (x ∈ ω → B ≼ x))
42		endomtr 3325	. . . . . . . . . . . . . . 15 ⊢ ((suc x ≈ B ∧ B ≼ x) → suc x ≼ x)
43		sssucid 2300	. . . . . . . . . . . . . . . 16 ⊢ x ⊆ suc x
44		ssdom2g 3312	. . . . . . . . . . . . . . . 16 ⊢ (suc x ∈ V → (x ⊆ suc x → x ≼ suc x))
45	23, 43, 44	mp2 43	. . . . . . . . . . . . . . 15 ⊢ x ≼ suc x
46	42, 45	jctir 241	. . . . . . . . . . . . . 14 ⊢ ((suc x ≈ B ∧ B ≼ x) → (suc x ≼ x ∧ x ≼ suc x))
47		sbth 3359	. . . . . . . . . . . . . 14 ⊢ ((suc x ≼ x ∧ x ≼ suc x) → suc x ≈ x)
48	46, 47	syl 12	. . . . . . . . . . . . 13 ⊢ ((suc x ≈ B ∧ B ≼ x) → suc x ≈ x)
49	48	exp 291	. . . . . . . . . . . 12 ⊢ (suc x ≈ B → (B ≼ x → suc x ≈ x))
50	49	com12 13	. . . . . . . . . . 11 ⊢ (B ≼ x → (suc x ≈ B → suc x ≈ x))
51		peano2b 2388	. . . . . . . . . . . . . 14 ⊢ (x ∈ ω ↔ suc x ∈ ω)
52		nnord 2381	. . . . . . . . . . . . . 14 ⊢ (suc x ∈ ω → Ord suc x)
53	51, 52	sylbi 174	. . . . . . . . . . . . 13 ⊢ (x ∈ ω → Ord suc x)
54	22	sucid 2304	. . . . . . . . . . . . . 14 ⊢ x ∈ suc x
55		nordeq 2218	. . . . . . . . . . . . . 14 ⊢ ((Ord suc x ∧ x ∈ suc x) → ¬ suc x = x)
56	54, 55	mpan2 519	. . . . . . . . . . . . 13 ⊢ (Ord suc x → ¬ suc x = x)
57	53, 56	syl 12	. . . . . . . . . . . 12 ⊢ (x ∈ ω → ¬ suc x = x)
58		nneneq 3408	. . . . . . . . . . . . . 14 ⊢ ((suc x ∈ ω ∧ x ∈ ω) → (suc x ≈ x ↔ suc x = x))
59	58, 51	sylanb 344	. . . . . . . . . . . . 13 ⊢ ((x ∈ ω ∧ x ∈ ω) → (suc x ≈ x ↔ suc x = x))
60	59	anidms 332	. . . . . . . . . . . 12 ⊢ (x ∈ ω → (suc x ≈ x ↔ suc x = x))
61	57, 60	mtbird 537	. . . . . . . . . . 11 ⊢ (x ∈ ω → ¬ suc x ≈ x)
62	50, 61	nsyli 106	. . . . . . . . . 10 ⊢ (B ≼ x → (x ∈ ω → ¬ suc x ≈ B))
63	41, 62	syli 52	. . . . . . . . 9 ⊢ (B ⊂ suc x → (x ∈ ω → ¬ suc x ≈ B))
64	63	com12 13	. . . . . . . 8 ⊢ (x ∈ ω → (B ⊂ suc x → ¬ suc x ≈ B))
65	12, 64	syl5bir 184	. . . . . . 7 ⊢ (A = suc x → (x ∈ ω → (B ⊂ A → ¬ A ≈ B)))
66	65	com12 13	. . . . . 6 ⊢ (x ∈ ω → (A = suc x → (B ⊂ A → ¬ A ≈ B)))
67	66	r19.23aiv 1284	. . . . 5 ⊢ (∃x ∈ ω A = suc x → (B ⊂ A → ¬ A ≈ B))
68	8, 67	syl 12	. . . 4 ⊢ ((A ∈ ω ∧ B ⊂ A) → (B ⊂ A → ¬ A ≈ B))
69	68	exp 291	. . 3 ⊢ (A ∈ ω → (B ⊂ A → (B ⊂ A → ¬ A ≈ B)))
70	69	pm2.43d 59	. 2 ⊢ (A ∈ ω → (B ⊂ A → ¬ A ≈ B))
71	70	imp 277	1 ⊢ ((A ∈ ω ∧ B ⊂ A) → ¬ A ≈ B)

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∃wex 678   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  Vcvv 1348   ∖ cdif 1484   ∩ cin 1486   ⊆ wss 1487   ⊂ wpss 1488  ∅c0 1707  {csn 1808   class class class wbr 2054  Ord word 2198  suc csuc 2201  ωcom 2372   ≈ cen 3271   ≼ cdom 3272

This theorem is referenced by:  php2 3410  php3 3411

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-er 3200  df-en 3274  df-dom 3275

metamath.org