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

Theorem php 8434
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 8429 through phplem4 8432, nneneq 8433, 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 4198 . . . . . . . 8 ∅ ⊆ 𝐵
2 sspsstr 3934 . . . . . . . 8 ((∅ ⊆ 𝐵𝐵𝐴) → ∅ ⊊ 𝐴)
31, 2mpan 680 . . . . . . 7 (𝐵𝐴 → ∅ ⊊ 𝐴)
4 0pss 4239 . . . . . . . 8 (∅ ⊊ 𝐴𝐴 ≠ ∅)
5 df-ne 2970 . . . . . . . 8 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
64, 5bitri 267 . . . . . . 7 (∅ ⊊ 𝐴 ↔ ¬ 𝐴 = ∅)
73, 6sylib 210 . . . . . 6 (𝐵𝐴 → ¬ 𝐴 = ∅)
8 nn0suc 7370 . . . . . . 7 (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑥 ∈ ω 𝐴 = suc 𝑥))
98orcanai 988 . . . . . 6 ((𝐴 ∈ ω ∧ ¬ 𝐴 = ∅) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥)
107, 9sylan2 586 . . . . 5 ((𝐴 ∈ ω ∧ 𝐵𝐴) → ∃𝑥 ∈ ω 𝐴 = suc 𝑥)
11 pssnel 4263 . . . . . . . . . 10 (𝐵 ⊊ suc 𝑥 → ∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦𝐵))
12 pssss 3924 . . . . . . . . . . . . . . . . 17 (𝐵 ⊊ suc 𝑥𝐵 ⊆ suc 𝑥)
13 ssdif 3968 . . . . . . . . . . . . . . . . . 18 (𝐵 ⊆ suc 𝑥 → (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦}))
14 disjsn 4478 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦𝐵)
15 disj3 4246 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∩ {𝑦}) = ∅ ↔ 𝐵 = (𝐵 ∖ {𝑦}))
1614, 15bitr3i 269 . . . . . . . . . . . . . . . . . . 19 𝑦𝐵𝐵 = (𝐵 ∖ {𝑦}))
17 sseq1 3845 . . . . . . . . . . . . . . . . . . 19 (𝐵 = (𝐵 ∖ {𝑦}) → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦})))
1816, 17sylbi 209 . . . . . . . . . . . . . . . . . 18 𝑦𝐵 → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) ↔ (𝐵 ∖ {𝑦}) ⊆ (suc 𝑥 ∖ {𝑦})))
1913, 18syl5ibr 238 . . . . . . . . . . . . . . . . 17 𝑦𝐵 → (𝐵 ⊆ suc 𝑥𝐵 ⊆ (suc 𝑥 ∖ {𝑦})))
20 vex 3401 . . . . . . . . . . . . . . . . . . . 20 𝑥 ∈ V
2120sucex 7291 . . . . . . . . . . . . . . . . . . 19 suc 𝑥 ∈ V
2221difexi 5048 . . . . . . . . . . . . . . . . . 18 (suc 𝑥 ∖ {𝑦}) ∈ V
23 ssdomg 8289 . . . . . . . . . . . . . . . . . 18 ((suc 𝑥 ∖ {𝑦}) ∈ V → (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦})))
2422, 23ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝐵 ⊆ (suc 𝑥 ∖ {𝑦}) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))
2512, 19, 24syl56 36 . . . . . . . . . . . . . . . 16 𝑦𝐵 → (𝐵 ⊊ suc 𝑥𝐵 ≼ (suc 𝑥 ∖ {𝑦})))
2625imp 397 . . . . . . . . . . . . . . 15 ((¬ 𝑦𝐵𝐵 ⊊ suc 𝑥) → 𝐵 ≼ (suc 𝑥 ∖ {𝑦}))
27 vex 3401 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
2820, 27phplem3 8431 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → 𝑥 ≈ (suc 𝑥 ∖ {𝑦}))
2928ensymd 8294 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥) → (suc 𝑥 ∖ {𝑦}) ≈ 𝑥)
30 domentr 8302 . . . . . . . . . . . . . . 15 ((𝐵 ≼ (suc 𝑥 ∖ {𝑦}) ∧ (suc 𝑥 ∖ {𝑦}) ≈ 𝑥) → 𝐵𝑥)
3126, 29, 30syl2an 589 . . . . . . . . . . . . . 14 (((¬ 𝑦𝐵𝐵 ⊊ suc 𝑥) ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥)) → 𝐵𝑥)
3231exp43 429 . . . . . . . . . . . . 13 𝑦𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → (𝑦 ∈ suc 𝑥𝐵𝑥))))
3332com4r 94 . . . . . . . . . . . 12 (𝑦 ∈ suc 𝑥 → (¬ 𝑦𝐵 → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵𝑥))))
3433imp 397 . . . . . . . . . . 11 ((𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵𝑥)))
3534exlimiv 1973 . . . . . . . . . 10 (∃𝑦(𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦𝐵) → (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵𝑥)))
3611, 35mpcom 38 . . . . . . . . 9 (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → 𝐵𝑥))
37 endomtr 8301 . . . . . . . . . . . 12 ((suc 𝑥𝐵𝐵𝑥) → suc 𝑥𝑥)
38 sssucid 6055 . . . . . . . . . . . . 13 𝑥 ⊆ suc 𝑥
39 ssdomg 8289 . . . . . . . . . . . . 13 (suc 𝑥 ∈ V → (𝑥 ⊆ suc 𝑥𝑥 ≼ suc 𝑥))
4021, 38, 39mp2 9 . . . . . . . . . . . 12 𝑥 ≼ suc 𝑥
41 sbth 8370 . . . . . . . . . . . 12 ((suc 𝑥𝑥𝑥 ≼ suc 𝑥) → suc 𝑥𝑥)
4237, 40, 41sylancl 580 . . . . . . . . . . 11 ((suc 𝑥𝐵𝐵𝑥) → suc 𝑥𝑥)
4342expcom 404 . . . . . . . . . 10 (𝐵𝑥 → (suc 𝑥𝐵 → suc 𝑥𝑥))
44 peano2b 7361 . . . . . . . . . . . . 13 (𝑥 ∈ ω ↔ suc 𝑥 ∈ ω)
45 nnord 7353 . . . . . . . . . . . . 13 (suc 𝑥 ∈ ω → Ord suc 𝑥)
4644, 45sylbi 209 . . . . . . . . . . . 12 (𝑥 ∈ ω → Ord suc 𝑥)
4720sucid 6057 . . . . . . . . . . . 12 𝑥 ∈ suc 𝑥
48 nordeq 5997 . . . . . . . . . . . 12 ((Ord suc 𝑥𝑥 ∈ suc 𝑥) → suc 𝑥𝑥)
4946, 47, 48sylancl 580 . . . . . . . . . . 11 (𝑥 ∈ ω → suc 𝑥𝑥)
50 nneneq 8433 . . . . . . . . . . . . . 14 ((suc 𝑥 ∈ ω ∧ 𝑥 ∈ ω) → (suc 𝑥𝑥 ↔ suc 𝑥 = 𝑥))
5144, 50sylanb 576 . . . . . . . . . . . . 13 ((𝑥 ∈ ω ∧ 𝑥 ∈ ω) → (suc 𝑥𝑥 ↔ suc 𝑥 = 𝑥))
5251anidms 562 . . . . . . . . . . . 12 (𝑥 ∈ ω → (suc 𝑥𝑥 ↔ suc 𝑥 = 𝑥))
5352necon3bbid 3006 . . . . . . . . . . 11 (𝑥 ∈ ω → (¬ suc 𝑥𝑥 ↔ suc 𝑥𝑥))
5449, 53mpbird 249 . . . . . . . . . 10 (𝑥 ∈ ω → ¬ suc 𝑥𝑥)
5543, 54nsyli 157 . . . . . . . . 9 (𝐵𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥𝐵))
5636, 55syli 39 . . . . . . . 8 (𝐵 ⊊ suc 𝑥 → (𝑥 ∈ ω → ¬ suc 𝑥𝐵))
5756com12 32 . . . . . . 7 (𝑥 ∈ ω → (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥𝐵))
58 psseq2 3917 . . . . . . . 8 (𝐴 = suc 𝑥 → (𝐵𝐴𝐵 ⊊ suc 𝑥))
59 breq1 4891 . . . . . . . . 9 (𝐴 = suc 𝑥 → (𝐴𝐵 ↔ suc 𝑥𝐵))
6059notbid 310 . . . . . . . 8 (𝐴 = suc 𝑥 → (¬ 𝐴𝐵 ↔ ¬ suc 𝑥𝐵))
6158, 60imbi12d 336 . . . . . . 7 (𝐴 = suc 𝑥 → ((𝐵𝐴 → ¬ 𝐴𝐵) ↔ (𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥𝐵)))
6257, 61syl5ibrcom 239 . . . . . 6 (𝑥 ∈ ω → (𝐴 = suc 𝑥 → (𝐵𝐴 → ¬ 𝐴𝐵)))
6362rexlimiv 3209 . . . . 5 (∃𝑥 ∈ ω 𝐴 = suc 𝑥 → (𝐵𝐴 → ¬ 𝐴𝐵))
6410, 63syl 17 . . . 4 ((𝐴 ∈ ω ∧ 𝐵𝐴) → (𝐵𝐴 → ¬ 𝐴𝐵))
6564ex 403 . . 3 (𝐴 ∈ ω → (𝐵𝐴 → (𝐵𝐴 → ¬ 𝐴𝐵)))
6665pm2.43d 53 . 2 (𝐴 ∈ ω → (𝐵𝐴 → ¬ 𝐴𝐵))
6766imp 397 1 ((𝐴 ∈ ω ∧ 𝐵𝐴) → ¬ 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386   = wceq 1601  wex 1823  wcel 2107  wne 2969  wrex 3091  Vcvv 3398  cdif 3789  cin 3791  wss 3792  wpss 3793  c0 4141  {csn 4398   class class class wbr 4888  Ord word 5977  suc csuc 5980  ωcom 7345  cen 8240  cdom 8241
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-om 7346  df-er 8028  df-en 8244  df-dom 8245
This theorem is referenced by:  php2  8435  php3  8436
  Copyright terms: Public domain W3C validator