MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  php Structured version   Visualization version   GIF version

Theorem php 8104
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 8099 through phplem4 8102, nneneq 8103, 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.
StepHypRef Expression
1 0ss 3950 . . . . . . . 8 ∅ ⊆ 𝐵
2 sspsstr 3696 . . . . . . . 8 ((∅ ⊆ 𝐵𝐵𝐴) → ∅ ⊊ 𝐴)
31, 2mpan 705 . . . . . . 7 (𝐵𝐴 → ∅ ⊊ 𝐴)
4 0pss 3991 . . . . . . . 8 (∅ ⊊ 𝐴𝐴 ≠ ∅)
5 df-ne 2791 . . . . . . . 8 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
64, 5bitri 264 . . . . . . 7 (∅ ⊊ 𝐴 ↔ ¬ 𝐴 = ∅)
73, 6sylib 208 . . . . . 6 (𝐵𝐴 → ¬ 𝐴 = ∅)
8 nn0suc 7052 . . . . . . 7 (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))
98orcanai 951 . . . . . 6 ((𝐴 ∈ ω ∧ ¬ 𝐴 = ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥)
107, 9sylan2 491 . . . . 5 ((𝐴 ∈ ω ∧ 𝐵𝐴) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥)
11 pssnel 4017 . . . . . . . . . 10 (𝐵 ⊊ suc 𝑥 → ∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦𝐵))
12 pssss 3686 . . . . . . . . . . . . . . . . 17 (𝐵 ⊊ suc 𝑥𝐵 ⊆ suc 𝑥)
13 ssdif 3729 . . . . . . . . . . . . . . . . . 18 (𝐵 ⊆ suc 𝑥 → (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦}))
14 disjsn 4223 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦𝐵)
15 disj3 3999 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∩ {𝑦}) = ∅ ↔ 𝐵 = (𝐵 ∖ {𝑦}))
1614, 15bitr3i 266 . . . . . . . . . . . . . . . . . . 19 𝑦𝐵𝐵 = (𝐵 ∖ {𝑦}))
17 sseq1 3611 . . . . . . . . . . . . . . . . . . 19 (𝐵 = (𝐵 ∖ {𝑦}) → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦})))
1816, 17sylbi 207 . . . . . . . . . . . . . . . . . 18 𝑦𝐵 → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦})))
1913, 18syl5ibr 236 . . . . . . . . . . . . . . . . 17 𝑦𝐵 → (𝐵 ⊆ suc 𝑥𝐵 ⊆ (suc 𝑥 ∖ {𝑦})))
20 vex 3193 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
2120sucex 6973 . . . . . . . . . . . . . . . . . . 19 suc 𝑥 ∈ V
22 difss 3721 . . . . . . . . . . . . . . . . . . 19 (suc 𝑥 ∖ {𝑦}) ⊆ suc 𝑥
2321, 22ssexi 4773 . . . . . . . . . . . . . . . . . 18 (suc 𝑥 ∖ {𝑦}) ∈ V
24 ssdomg 7961 . . . . . . . . . . . . . . . . . 18 ((suc 𝑥 ∖ {𝑦}) ∈ V → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})))
2523, 24ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))
2612, 19, 25syl56 36 . . . . . . . . . . . . . . . 16 𝑦𝐵 → (𝐵 ⊊ suc 𝑥𝐵 ≼ (suc 𝑥 ∖ {𝑦})))
2726imp 445 . . . . . . . . . . . . . . 15 ((¬ 𝑦𝐵𝐵 ⊊ suc 𝑥) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))
28 vex 3193 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
2920, 28phplem3 8101 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → 𝑥 ≈ (suc 𝑥 ∖ {𝑦}))
3029ensymd 7967 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → (suc 𝑥 ∖ {𝑦}) ≈ 𝑥)
31 domentr 7975 . . . . . . . . . . . . . . 15 ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (suc 𝑥 ∖ {𝑦}) ≈ 𝑥) → 𝐵𝑥)
3227, 30, 31syl2an 494 . . . . . . . . . . . . . 14 (((¬ 𝑦𝐵𝐵 ⊊ suc 𝑥) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵𝑥)
3332exp43 639 . . . . . . . . . . . . 13 𝑦𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → (𝑦 ∈ suc 𝑥𝐵𝑥))))
3433com4r 94 . . . . . . . . . . . 12 (𝑦 ∈ suc 𝑥 → (¬ 𝑦𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵𝑥))))
3534imp 445 . . . . . . . . . . 11 ((𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵𝑥)))
3635exlimiv 1855 . . . . . . . . . 10 (∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵𝑥)))
3711, 36mpcom 38 . . . . . . . . 9 (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵𝑥))
38 endomtr 7974 . . . . . . . . . . . 12 ((suc 𝑥𝐵𝐵𝑥) → suc 𝑥𝑥)
39 sssucid 5771 . . . . . . . . . . . . 13 𝑥 ⊆ suc 𝑥
40 ssdomg 7961 . . . . . . . . . . . . 13 (suc 𝑥 ∈ V → (𝑥 ⊆ suc 𝑥𝑥 ≼ suc 𝑥))
4121, 39, 40mp2 9 . . . . . . . . . . . 12 𝑥 ≼ suc 𝑥
42 sbth 8040 . . . . . . . . . . . 12 ((suc 𝑥𝑥𝑥 ≼ suc 𝑥) → suc 𝑥𝑥)
4338, 41, 42sylancl 693 . . . . . . . . . . 11 ((suc 𝑥𝐵𝐵𝑥) → suc 𝑥𝑥)
4443expcom 451 . . . . . . . . . 10 (𝐵𝑥 → (suc 𝑥𝐵 → suc 𝑥𝑥))
45 peano2b 7043 . . . . . . . . . . . . 13 (𝑥 ∈ ω ↔ suc 𝑥 ∈ ω)
46 nnord 7035 . . . . . . . . . . . . 13 (suc 𝑥 ∈ ω → Ord suc 𝑥)
4745, 46sylbi 207 . . . . . . . . . . . 12 (𝑥 ∈ ω → Ord suc 𝑥)
4820sucid 5773 . . . . . . . . . . . 12 𝑥 ∈ suc 𝑥
49 nordeq 5711 . . . . . . . . . . . 12 ((Ord suc 𝑥𝑥 ∈ suc 𝑥) → suc 𝑥𝑥)
5047, 48, 49sylancl 693 . . . . . . . . . . 11 (𝑥 ∈ ω → suc 𝑥𝑥)
51 nneneq 8103 . . . . . . . . . . . . . 14 ((suc 𝑥 ∈ ω ∧ 𝑥 ∈ ω) → (suc 𝑥𝑥 ↔ suc 𝑥 = 𝑥))
5245, 51sylanb 489 . . . . . . . . . . . . 13 ((𝑥 ∈ ω ∧ 𝑥 ∈ ω) → (suc 𝑥𝑥 ↔ suc 𝑥 = 𝑥))
5352anidms 676 . . . . . . . . . . . 12 (𝑥 ∈ ω → (suc 𝑥𝑥 ↔ suc 𝑥 = 𝑥))
5453necon3bbid 2827 . . . . . . . . . . 11 (𝑥 ∈ ω → (¬ suc 𝑥𝑥 ↔ suc 𝑥𝑥))
5550, 54mpbird 247 . . . . . . . . . 10 (𝑥 ∈ ω → ¬ suc 𝑥𝑥)
5644, 55nsyli 155 . . . . . . . . 9 (𝐵𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥𝐵))
5737, 56syli 39 . . . . . . . 8 (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥𝐵))
5857com12 32 . . . . . . 7 (𝑥 ∈ ω → (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥𝐵))
59 psseq2 3679 . . . . . . . 8 (𝐴 = suc 𝑥 → (𝐵𝐴𝐵 ⊊ suc 𝑥))
60 breq1 4626 . . . . . . . . 9 (𝐴 = suc 𝑥 → (𝐴𝐵 ↔ suc 𝑥𝐵))
6160notbid 308 . . . . . . . 8 (𝐴 = suc 𝑥 → (¬ 𝐴𝐵 ↔ ¬ suc 𝑥𝐵))
6259, 61imbi12d 334 . . . . . . 7 (𝐴 = suc 𝑥 → ((𝐵𝐴 → ¬ 𝐴𝐵) ↔ (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥𝐵)))
6358, 62syl5ibrcom 237 . . . . . 6 (𝑥 ∈ ω → (𝐴 = suc 𝑥 → (𝐵𝐴 → ¬ 𝐴𝐵)))
6463rexlimiv 3022 . . . . 5 (∃𝑥 ∈ ω 𝐴 = suc 𝑥 → (𝐵𝐴 → ¬ 𝐴𝐵))
6510, 64syl 17 . . . 4 ((𝐴 ∈ ω ∧ 𝐵𝐴) → (𝐵𝐴 → ¬ 𝐴𝐵))
6665ex 450 . . 3 (𝐴 ∈ ω → (𝐵𝐴 → (𝐵𝐴 → ¬ 𝐴𝐵)))
6766pm2.43d 53 . 2 (𝐴 ∈ ω → (𝐵𝐴 → ¬ 𝐴𝐵))
6867imp 445 1 ((𝐴 ∈ ω ∧ 𝐵𝐴) → ¬ 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1987  wne 2790  wrex 2909  Vcvv 3190  cdif 3557  cin 3559  wss 3560  wpss 3561  c0 3897  {csn 4155   class class class wbr 4623  Ord word 5691  suc csuc 5694  ωcom 7027  cen 7912  cdom 7913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-om 7028  df-er 7702  df-en 7916  df-dom 7917
This theorem is referenced by:  php2  8105  php3  8106
  Copyright terms: Public domain W3C validator