ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  phpm GIF version

Theorem phpm 6921
Description: Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. By "proper subset" here we mean that there is an element which is in the natural number and not in the subset, or in symbols 𝑥𝑥 ∈ (𝐴𝐵) (which is stronger than not being equal in the absence of excluded middle). 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 6908 through phplem4 6911, nneneq 6913, and this final piece of the proof. (Contributed by NM, 29-May-1998.)
Assertion
Ref Expression
phpm ((𝐴 ∈ ω ∧ 𝐵𝐴 ∧ ∃𝑥 𝑥 ∈ (𝐴𝐵)) → ¬ 𝐴𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem phpm
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 simpr 110 . . . . . 6 ((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝐴 = ∅) → 𝐴 = ∅)
2 eldifi 3281 . . . . . . . . 9 (𝑥 ∈ (𝐴𝐵) → 𝑥𝐴)
3 ne0i 3453 . . . . . . . . 9 (𝑥𝐴𝐴 ≠ ∅)
42, 3syl 14 . . . . . . . 8 (𝑥 ∈ (𝐴𝐵) → 𝐴 ≠ ∅)
54neneqd 2385 . . . . . . 7 (𝑥 ∈ (𝐴𝐵) → ¬ 𝐴 = ∅)
65ad2antlr 489 . . . . . 6 ((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝐴 = ∅) → ¬ 𝐴 = ∅)
71, 6pm2.21dd 621 . . . . 5 ((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝐴 = ∅) → ¬ 𝐴𝐵)
8 php5dom 6919 . . . . . . . . . 10 (𝑦 ∈ ω → ¬ suc 𝑦𝑦)
98ad2antlr 489 . . . . . . . . 9 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → ¬ suc 𝑦𝑦)
10 simplr 528 . . . . . . . . . 10 ((((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴𝐵) → 𝐴 = suc 𝑦)
11 simpr 110 . . . . . . . . . . 11 ((((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴𝐵) → 𝐴𝐵)
12 vex 2763 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
1312sucex 4531 . . . . . . . . . . . . . . 15 suc 𝑦 ∈ V
14 difss 3285 . . . . . . . . . . . . . . 15 (suc 𝑦 ∖ {𝑥}) ⊆ suc 𝑦
1513, 14ssexi 4167 . . . . . . . . . . . . . 14 (suc 𝑦 ∖ {𝑥}) ∈ V
16 eldifn 3282 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴𝐵) → ¬ 𝑥𝐵)
1716ad3antlr 493 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → ¬ 𝑥𝐵)
18 simpllr 534 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) → 𝐵𝐴)
1918adantr 276 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵𝐴)
20 simpr 110 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐴 = suc 𝑦)
2119, 20sseqtrd 3217 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ⊆ suc 𝑦)
22 ssdif 3294 . . . . . . . . . . . . . . . 16 (𝐵 ⊆ suc 𝑦 → (𝐵 ∖ {𝑥}) ⊆ (suc 𝑦 ∖ {𝑥}))
23 disjsn 3680 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥𝐵)
24 disj3 3499 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∩ {𝑥}) = ∅ ↔ 𝐵 = (𝐵 ∖ {𝑥}))
2523, 24bitr3i 186 . . . . . . . . . . . . . . . . 17 𝑥𝐵𝐵 = (𝐵 ∖ {𝑥}))
26 sseq1 3202 . . . . . . . . . . . . . . . . 17 (𝐵 = (𝐵 ∖ {𝑥}) → (𝐵 ⊆ (suc 𝑦 ∖ {𝑥}) ↔ (𝐵 ∖ {𝑥}) ⊆ (suc 𝑦 ∖ {𝑥})))
2725, 26sylbi 121 . . . . . . . . . . . . . . . 16 𝑥𝐵 → (𝐵 ⊆ (suc 𝑦 ∖ {𝑥}) ↔ (𝐵 ∖ {𝑥}) ⊆ (suc 𝑦 ∖ {𝑥})))
2822, 27imbitrrid 156 . . . . . . . . . . . . . . 15 𝑥𝐵 → (𝐵 ⊆ suc 𝑦𝐵 ⊆ (suc 𝑦 ∖ {𝑥})))
2917, 21, 28sylc 62 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ⊆ (suc 𝑦 ∖ {𝑥}))
30 ssdomg 6832 . . . . . . . . . . . . . 14 ((suc 𝑦 ∖ {𝑥}) ∈ V → (𝐵 ⊆ (suc 𝑦 ∖ {𝑥}) → 𝐵 ≼ (suc 𝑦 ∖ {𝑥})))
3115, 29, 30mpsyl 65 . . . . . . . . . . . . 13 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵 ≼ (suc 𝑦 ∖ {𝑥}))
32 simplr 528 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝑦 ∈ ω)
332ad3antlr 493 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝑥𝐴)
3433, 20eleqtrd 2272 . . . . . . . . . . . . . 14 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝑥 ∈ suc 𝑦)
35 phplem3g 6912 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ω ∧ 𝑥 ∈ suc 𝑦) → 𝑦 ≈ (suc 𝑦 ∖ {𝑥}))
3635ensymd 6837 . . . . . . . . . . . . . 14 ((𝑦 ∈ ω ∧ 𝑥 ∈ suc 𝑦) → (suc 𝑦 ∖ {𝑥}) ≈ 𝑦)
3732, 34, 36syl2anc 411 . . . . . . . . . . . . 13 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → (suc 𝑦 ∖ {𝑥}) ≈ 𝑦)
38 domentr 6845 . . . . . . . . . . . . 13 ((𝐵 ≼ (suc 𝑦 ∖ {𝑥}) ∧ (suc 𝑦 ∖ {𝑥}) ≈ 𝑦) → 𝐵𝑦)
3931, 37, 38syl2anc 411 . . . . . . . . . . . 12 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → 𝐵𝑦)
4039adantr 276 . . . . . . . . . . 11 ((((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴𝐵) → 𝐵𝑦)
41 endomtr 6844 . . . . . . . . . . 11 ((𝐴𝐵𝐵𝑦) → 𝐴𝑦)
4211, 40, 41syl2anc 411 . . . . . . . . . 10 ((((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴𝐵) → 𝐴𝑦)
4310, 42eqbrtrrd 4053 . . . . . . . . 9 ((((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) ∧ 𝐴𝐵) → suc 𝑦𝑦)
449, 43mtand 666 . . . . . . . 8 (((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) ∧ 𝐴 = suc 𝑦) → ¬ 𝐴𝐵)
4544ex 115 . . . . . . 7 ((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ 𝑦 ∈ ω) → (𝐴 = suc 𝑦 → ¬ 𝐴𝐵))
4645rexlimdva 2611 . . . . . 6 (((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) → (∃𝑦 ∈ ω 𝐴 = suc 𝑦 → ¬ 𝐴𝐵))
4746imp 124 . . . . 5 ((((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) ∧ ∃𝑦 ∈ ω 𝐴 = suc 𝑦) → ¬ 𝐴𝐵)
48 nn0suc 4636 . . . . . 6 (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑦 ∈ ω 𝐴 = suc 𝑦))
4948ad2antrr 488 . . . . 5 (((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) → (𝐴 = ∅ ∨ ∃𝑦 ∈ ω 𝐴 = suc 𝑦))
507, 47, 49mpjaodan 799 . . . 4 (((𝐴 ∈ ω ∧ 𝐵𝐴) ∧ 𝑥 ∈ (𝐴𝐵)) → ¬ 𝐴𝐵)
5150ex 115 . . 3 ((𝐴 ∈ ω ∧ 𝐵𝐴) → (𝑥 ∈ (𝐴𝐵) → ¬ 𝐴𝐵))
5251exlimdv 1830 . 2 ((𝐴 ∈ ω ∧ 𝐵𝐴) → (∃𝑥 𝑥 ∈ (𝐴𝐵) → ¬ 𝐴𝐵))
53523impia 1202 1 ((𝐴 ∈ ω ∧ 𝐵𝐴 ∧ ∃𝑥 𝑥 ∈ (𝐴𝐵)) → ¬ 𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  w3a 980   = wceq 1364  wex 1503  wcel 2164  wne 2364  wrex 2473  Vcvv 2760  cdif 3150  cin 3152  wss 3153  c0 3446  {csn 3618   class class class wbr 4029  suc csuc 4396  ωcom 4622  cen 6792  cdom 6793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-iinf 4620
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-sbc 2986  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-br 4030  df-opab 4091  df-tr 4128  df-id 4324  df-iord 4397  df-on 4399  df-suc 4402  df-iom 4623  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-er 6587  df-en 6795  df-dom 6796
This theorem is referenced by:  phpelm  6922
  Copyright terms: Public domain W3C validator