Theorem php 8704

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 8699 through phplem4 8702, nneneq 8703, and this final piece of the proof. (Contributed by NM, 29-May-1998.)

Assertion

Ref	Expression
php	⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵)

Proof of Theorem php

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ss 4353	. . . . . . . 8 ⊢ ∅ ⊆ 𝐵
2		sspsstr 4085	. . . . . . . 8 ⊢ ((∅ ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐴) → ∅ ⊊ 𝐴)
3	1, 2	mpan 688	. . . . . . 7 ⊢ (𝐵 ⊊ 𝐴 → ∅ ⊊ 𝐴)
4		0pss 4399	. . . . . . . 8 ⊢ (∅ ⊊ 𝐴 ↔ 𝐴 ≠ ∅)
5		df-ne 3020	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
6	4, 5	bitri 277	. . . . . . 7 ⊢ (∅ ⊊ 𝐴 ↔ ¬ 𝐴 = ∅)
7	3, 6	sylib 220	. . . . . 6 ⊢ (𝐵 ⊊ 𝐴 → ¬ 𝐴 = ∅)
8		nn0suc 7609	. . . . . . 7 ⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))
9	8	orcanai 999	. . . . . 6 ⊢ ((𝐴 ∈ ω ∧ ¬ 𝐴 = ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥)
10	7, 9	sylan2 594	. . . . 5 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥)
11		pssnel 4423	. . . . . . . . . 10 ⊢ (𝐵 ⊊ suc 𝑥 → ∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵))
12		pssss 4075	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ⊊ suc 𝑥 → 𝐵 ⊆ suc 𝑥)
13		ssdif 4119	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ⊆ suc 𝑥 → (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦}))
14		disjsn 4650	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦 ∈ 𝐵)
15		disj3 4406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∩ {𝑦}) = ∅ ↔ 𝐵 = (𝐵 ∖ {𝑦}))
16	14, 15	bitr3i 279	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑦 ∈ 𝐵 ↔ 𝐵 = (𝐵 ∖ {𝑦}))
17		sseq1 3995	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 = (𝐵 ∖ {𝑦}) → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦})))
18	16, 17	sylbi 219	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑦 ∈ 𝐵 → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦})))
19	13, 18	syl5ibr 248	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑦 ∈ 𝐵 → (𝐵 ⊆ suc 𝑥 → 𝐵 ⊆ (suc 𝑥 ∖ {𝑦})))
20		vex 3500	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑥 ∈ V
21	20	sucex 7529	. . . . . . . . . . . . . . . . . . 19 ⊢ suc 𝑥 ∈ V
22	21	difexi 5235	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑥 ∖ {𝑦}) ∈ V
23		ssdomg 8558	. . . . . . . . . . . . . . . . . 18 ⊢ ((suc 𝑥 ∖ {𝑦}) ∈ V → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})))
24	22, 23	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))
25	12, 19, 24	syl56 36	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑦 ∈ 𝐵 → (𝐵 ⊊ suc 𝑥 → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})))
26	25	imp 409	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))
27		vex 3500	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
28	20, 27	phplem3 8701	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → 𝑥 ≈ (suc 𝑥 ∖ {𝑦}))
29	28	ensymd 8563	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → (suc 𝑥 ∖ {𝑦}) ≈ 𝑥)
30		domentr 8571	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (suc 𝑥 ∖ {𝑦}) ≈ 𝑥) → 𝐵 ≼ 𝑥)
31	26, 29, 30	syl2an 597	. . . . . . . . . . . . . 14 ⊢ (((¬ 𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵 ≼ 𝑥)
32	31	exp43 439	. . . . . . . . . . . . 13 ⊢ (¬ 𝑦 ∈ 𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → (𝑦 ∈ suc 𝑥 → 𝐵 ≼ 𝑥))))
33	32	com4r 94	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ suc 𝑥 → (¬ 𝑦 ∈ 𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥))))
34	33	imp 409	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥)))
35	34	exlimiv 1930	. . . . . . . . . 10 ⊢ (∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥)))
36	11, 35	mpcom 38	. . . . . . . . 9 ⊢ (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵 ≼ 𝑥))
37		endomtr 8570	. . . . . . . . . . . 12 ⊢ ((suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥) → suc 𝑥 ≼ 𝑥)
38		sssucid 6271	. . . . . . . . . . . . 13 ⊢ 𝑥 ⊆ suc 𝑥
39		ssdomg 8558	. . . . . . . . . . . . 13 ⊢ (suc 𝑥 ∈ V → (𝑥 ⊆ suc 𝑥 → 𝑥 ≼ suc 𝑥))
40	21, 38, 39	mp2 9	. . . . . . . . . . . 12 ⊢ 𝑥 ≼ suc 𝑥
41		sbth 8640	. . . . . . . . . . . 12 ⊢ ((suc 𝑥 ≼ 𝑥 ∧ 𝑥 ≼ suc 𝑥) → suc 𝑥 ≈ 𝑥)
42	37, 40, 41	sylancl 588	. . . . . . . . . . 11 ⊢ ((suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥) → suc 𝑥 ≈ 𝑥)
43	42	expcom 416	. . . . . . . . . 10 ⊢ (𝐵 ≼ 𝑥 → (suc 𝑥 ≈ 𝐵 → suc 𝑥 ≈ 𝑥))
44		peano2b 7599	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ω ↔ suc 𝑥 ∈ ω)
45		nnord 7591	. . . . . . . . . . . . 13 ⊢ (suc 𝑥 ∈ ω → Ord suc 𝑥)
46	44, 45	sylbi 219	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ω → Ord suc 𝑥)
47	20	sucid 6273	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ suc 𝑥
48		nordeq 6213	. . . . . . . . . . . 12 ⊢ ((Ord suc 𝑥 ∧ 𝑥 ∈ suc 𝑥) → suc 𝑥 ≠ 𝑥)
49	46, 47, 48	sylancl 588	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ω → suc 𝑥 ≠ 𝑥)
50		nneneq 8703	. . . . . . . . . . . . . 14 ⊢ ((suc 𝑥 ∈ ω ∧ 𝑥 ∈ ω) → (suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥))
51	44, 50	sylanb 583	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ω ∧ 𝑥 ∈ ω) → (suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥))
52	51	anidms 569	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ω → (suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥))
53	52	necon3bbid 3056	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ω → (¬ suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 ≠ 𝑥))
54	49, 53	mpbird 259	. . . . . . . . . 10 ⊢ (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝑥)
55	43, 54	nsyli 160	. . . . . . . . 9 ⊢ (𝐵 ≼ 𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵))
56	36, 55	syli 39	. . . . . . . 8 ⊢ (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵))
57	56	com12 32	. . . . . . 7 ⊢ (𝑥 ∈ ω → (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵))
58		psseq2 4068	. . . . . . . 8 ⊢ (𝐴 = suc 𝑥 → (𝐵 ⊊ 𝐴 ↔ 𝐵 ⊊ suc 𝑥))
59		breq1 5072	. . . . . . . . 9 ⊢ (𝐴 = suc 𝑥 → (𝐴 ≈ 𝐵 ↔ suc 𝑥 ≈ 𝐵))
60	59	notbid 320	. . . . . . . 8 ⊢ (𝐴 = suc 𝑥 → (¬ 𝐴 ≈ 𝐵 ↔ ¬ suc 𝑥 ≈ 𝐵))
61	58, 60	imbi12d 347	. . . . . . 7 ⊢ (𝐴 = suc 𝑥 → ((𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵) ↔ (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵)))
62	57, 61	syl5ibrcom 249	. . . . . 6 ⊢ (𝑥 ∈ ω → (𝐴 = suc 𝑥 → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵)))
63	62	rexlimiv 3283	. . . . 5 ⊢ (∃𝑥 ∈ ω 𝐴 = suc 𝑥 → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵))
64	10, 63	syl 17	. . . 4 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵))
65	64	ex 415	. . 3 ⊢ (𝐴 ∈ ω → (𝐵 ⊊ 𝐴 → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵)))
66	65	pm2.43d 53	. 2 ⊢ (𝐴 ∈ ω → (𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵))
67	66	imp 409	1 ⊢ ((𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴) → ¬ 𝐴 ≈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1536  ∃wex 1779   ∈ wcel 2113   ≠ wne 3019  ∃wrex 3142  Vcvv 3497   ∖ cdif 3936   ∩ cin 3938   ⊆ wss 3939   ⊊ wpss 3940  ∅c0 4294  {csn 4570   class class class wbr 5069  Ord word 6193  suc csuc 6196  ωcom 7583   ≈ cen 8509   ≼ cdom 8510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-om 7584  df-er 8292  df-en 8513  df-dom 8514

This theorem is referenced by:  php2  8705  php3  8706  rr-phpd  40568