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

Theorem php 7840
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 7835 through phplem4 7838, nneneq 7839, 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 3802 . . . . . . . 8 ∅ ⊆ 𝐵
2 sspsstr 3560 . . . . . . . 8 ((∅ ⊆ 𝐵𝐵𝐴) → ∅ ⊊ 𝐴)
31, 2mpan 693 . . . . . . 7 (𝐵𝐴 → ∅ ⊊ 𝐴)
4 0pss 3842 . . . . . . . 8 (∅ ⊊ 𝐴𝐴 ≠ ∅)
5 df-ne 2677 . . . . . . . 8 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
64, 5bitri 259 . . . . . . 7 (∅ ⊊ 𝐴 ↔ ¬ 𝐴 = ∅)
73, 6sylib 203 . . . . . 6 (𝐵𝐴 → ¬ 𝐴 = ∅)
8 nn0suc 6794 . . . . . . 7 (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))
98orcanai 940 . . . . . 6 ((𝐴 ∈ ω ∧ ¬ 𝐴 = ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥)
107, 9sylan2 484 . . . . 5 ((𝐴 ∈ ω ∧ 𝐵𝐴) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥)
11 pssnel 3865 . . . . . . . . . 10 (𝐵 ⊊ suc 𝑥 → ∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦𝐵))
12 pssss 3550 . . . . . . . . . . . . . . . . 17 (𝐵 ⊊ suc 𝑥𝐵 ⊆ suc 𝑥)
13 ssdif 3593 . . . . . . . . . . . . . . . . . 18 (𝐵 ⊆ suc 𝑥 → (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦}))
14 disjsn 4060 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦𝐵)
15 disj3 3849 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∩ {𝑦}) = ∅ ↔ 𝐵 = (𝐵 ∖ {𝑦}))
1614, 15bitr3i 261 . . . . . . . . . . . . . . . . . . 19 𝑦𝐵𝐵 = (𝐵 ∖ {𝑦}))
17 sseq1 3475 . . . . . . . . . . . . . . . . . . 19 (𝐵 = (𝐵 ∖ {𝑦}) → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦})))
1816, 17sylbi 202 . . . . . . . . . . . . . . . . . 18 𝑦𝐵 → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦})))
1913, 18syl5ibr 231 . . . . . . . . . . . . . . . . 17 𝑦𝐵 → (𝐵 ⊆ suc 𝑥𝐵 ⊆ (suc 𝑥 ∖ {𝑦})))
20 vex 3069 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
2120sucex 6715 . . . . . . . . . . . . . . . . . . 19 suc 𝑥 ∈ V
22 difss 3585 . . . . . . . . . . . . . . . . . . 19 (suc 𝑥 ∖ {𝑦}) ⊆ suc 𝑥
2321, 22ssexi 4581 . . . . . . . . . . . . . . . . . 18 (suc 𝑥 ∖ {𝑦}) ∈ V
24 ssdomg 7698 . . . . . . . . . . . . . . . . . 18 ((suc 𝑥 ∖ {𝑦}) ∈ V → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})))
2523, 24ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))
2612, 19, 25syl56 35 . . . . . . . . . . . . . . . 16 𝑦𝐵 → (𝐵 ⊊ suc 𝑥𝐵 ≼ (suc 𝑥 ∖ {𝑦})))
2726imp 438 . . . . . . . . . . . . . . 15 ((¬ 𝑦𝐵𝐵 ⊊ suc 𝑥) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))
28 vex 3069 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
2920, 28phplem3 7837 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → 𝑥 ≈ (suc 𝑥 ∖ {𝑦}))
3029ensymd 7704 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → (suc 𝑥 ∖ {𝑦}) ≈ 𝑥)
31 domentr 7712 . . . . . . . . . . . . . . 15 ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (suc 𝑥 ∖ {𝑦}) ≈ 𝑥) → 𝐵𝑥)
3227, 30, 31syl2an 487 . . . . . . . . . . . . . 14 (((¬ 𝑦𝐵𝐵 ⊊ suc 𝑥) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵𝑥)
3332exp43 629 . . . . . . . . . . . . 13 𝑦𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → (𝑦 ∈ suc 𝑥𝐵𝑥))))
3433com4r 90 . . . . . . . . . . . 12 (𝑦 ∈ suc 𝑥 → (¬ 𝑦𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵𝑥))))
3534imp 438 . . . . . . . . . . 11 ((𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵𝑥)))
3635exlimiv 1807 . . . . . . . . . 10 (∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵𝑥)))
3711, 36mpcom 37 . . . . . . . . 9 (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵𝑥))
38 endomtr 7711 . . . . . . . . . . . 12 ((suc 𝑥𝐵𝐵𝑥) → suc 𝑥𝑥)
39 sssucid 5551 . . . . . . . . . . . . 13 𝑥 ⊆ suc 𝑥
40 ssdomg 7698 . . . . . . . . . . . . 13 (suc 𝑥 ∈ V → (𝑥 ⊆ suc 𝑥𝑥 ≼ suc 𝑥))
4121, 39, 40mp2 9 . . . . . . . . . . . 12 𝑥 ≼ suc 𝑥
42 sbth 7776 . . . . . . . . . . . 12 ((suc 𝑥𝑥𝑥 ≼ suc 𝑥) → suc 𝑥𝑥)
4338, 41, 42sylancl 684 . . . . . . . . . . 11 ((suc 𝑥𝐵𝐵𝑥) → suc 𝑥𝑥)
4443expcom 444 . . . . . . . . . 10 (𝐵𝑥 → (suc 𝑥𝐵 → suc 𝑥𝑥))
45 peano2b 6785 . . . . . . . . . . . . 13 (𝑥 ∈ ω ↔ suc 𝑥 ∈ ω)
46 nnord 6777 . . . . . . . . . . . . 13 (suc 𝑥 ∈ ω → Ord suc 𝑥)
4745, 46sylbi 202 . . . . . . . . . . . 12 (𝑥 ∈ ω → Ord suc 𝑥)
4820sucid 5553 . . . . . . . . . . . 12 𝑥 ∈ suc 𝑥
49 nordeq 5493 . . . . . . . . . . . 12 ((Ord suc 𝑥𝑥 ∈ suc 𝑥) → suc 𝑥𝑥)
5047, 48, 49sylancl 684 . . . . . . . . . . 11 (𝑥 ∈ ω → suc 𝑥𝑥)
51 nneneq 7839 . . . . . . . . . . . . . 14 ((suc 𝑥 ∈ ω ∧ 𝑥 ∈ ω) → (suc 𝑥𝑥 ↔ suc 𝑥 = 𝑥))
5245, 51sylanb 482 . . . . . . . . . . . . 13 ((𝑥 ∈ ω ∧ 𝑥 ∈ ω) → (suc 𝑥𝑥 ↔ suc 𝑥 = 𝑥))
5352anidms 666 . . . . . . . . . . . 12 (𝑥 ∈ ω → (suc 𝑥𝑥 ↔ suc 𝑥 = 𝑥))
5453necon3bbid 2714 . . . . . . . . . . 11 (𝑥 ∈ ω → (¬ suc 𝑥𝑥 ↔ suc 𝑥𝑥))
5550, 54mpbird 242 . . . . . . . . . 10 (𝑥 ∈ ω → ¬ suc 𝑥𝑥)
5644, 55nsyli 150 . . . . . . . . 9 (𝐵𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥𝐵))
5737, 56syli 38 . . . . . . . 8 (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥𝐵))
5857com12 32 . . . . . . 7 (𝑥 ∈ ω → (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥𝐵))
59 psseq2 3543 . . . . . . . 8 (𝐴 = suc 𝑥 → (𝐵𝐴𝐵 ⊊ suc 𝑥))
60 breq1 4437 . . . . . . . . 9 (𝐴 = suc 𝑥 → (𝐴𝐵 ↔ suc 𝑥𝐵))
6160notbid 303 . . . . . . . 8 (𝐴 = suc 𝑥 → (¬ 𝐴𝐵 ↔ ¬ suc 𝑥𝐵))
6259, 61imbi12d 329 . . . . . . 7 (𝐴 = suc 𝑥 → ((𝐵𝐴 → ¬ 𝐴𝐵) ↔ (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥𝐵)))
6358, 62syl5ibrcom 232 . . . . . 6 (𝑥 ∈ ω → (𝐴 = suc 𝑥 → (𝐵𝐴 → ¬ 𝐴𝐵)))
6463rexlimiv 2902 . . . . 5 (∃𝑥 ∈ ω 𝐴 = suc 𝑥 → (𝐵𝐴 → ¬ 𝐴𝐵))
6510, 64syl 17 . . . 4 ((𝐴 ∈ ω ∧ 𝐵𝐴) → (𝐵𝐴 → ¬ 𝐴𝐵))
6665ex 443 . . 3 (𝐴 ∈ ω → (𝐵𝐴 → (𝐵𝐴 → ¬ 𝐴𝐵)))
6766pm2.43d 50 . 2 (𝐴 ∈ ω → (𝐵𝐴 → ¬ 𝐴𝐵))
6867imp 438 1 ((𝐴 ∈ ω ∧ 𝐵𝐴) → ¬ 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 191  wa 378   = wceq 1468  wex 1692  wcel 1937  wne 2675  wrex 2792  Vcvv 3066  cdif 3423  cin 3425  wss 3426  wpss 3427  c0 3757  {csn 3995   class class class wbr 4434  Ord word 5473  suc csuc 5476  ωcom 6769  cen 7649  cdom 7650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-sbc 3292  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-br 4435  df-opab 4494  df-tr 4531  df-eprel 4791  df-id 4795  df-po 4801  df-so 4802  df-fr 4839  df-we 4841  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-iota 5597  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640  df-fv 5641  df-om 6770  df-er 7440  df-en 7653  df-dom 7654
This theorem is referenced by:  php2  7841  php3  7842
  Copyright terms: Public domain W3C validator