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

Theorem php3 9156
Description: Corollary of Pigeonhole Principle. If 𝐴 is finite and 𝐵 is a proper subset of 𝐴, the 𝐵 is strictly less numerous than 𝐴. Stronger version of Corollary 6C of [Enderton] p. 135. (Contributed by NM, 22-Aug-2008.) Avoid ax-pow 5320. (Revised by BTernaryTau, 26-Nov-2024.)
Assertion
Ref Expression
php3 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵𝐴)

Proof of Theorem php3
Dummy variables 𝑓 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 8916 . . 3 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
2 bren 8893 . . . . . 6 (𝐴𝑥 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝑥)
3 pssss 4055 . . . . . . . . . . . . . 14 (𝐵𝐴𝐵𝐴)
4 imass2 6054 . . . . . . . . . . . . . 14 (𝐵𝐴 → (𝑓𝐵) ⊆ (𝑓𝐴))
53, 4syl 17 . . . . . . . . . . . . 13 (𝐵𝐴 → (𝑓𝐵) ⊆ (𝑓𝐴))
65adantl 482 . . . . . . . . . . . 12 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵) ⊆ (𝑓𝐴))
7 pssnel 4430 . . . . . . . . . . . . . 14 (𝐵𝐴 → ∃𝑦(𝑦𝐴 ∧ ¬ 𝑦𝐵))
8 eldif 3920 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴 ∧ ¬ 𝑦𝐵))
9 f1ofn 6785 . . . . . . . . . . . . . . . . . . . 20 (𝑓:𝐴1-1-onto𝑥𝑓 Fn 𝐴)
10 difss 4091 . . . . . . . . . . . . . . . . . . . 20 (𝐴𝐵) ⊆ 𝐴
11 fnfvima 7183 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 Fn 𝐴 ∧ (𝐴𝐵) ⊆ 𝐴𝑦 ∈ (𝐴𝐵)) → (𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵)))
12113expia 1121 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 Fn 𝐴 ∧ (𝐴𝐵) ⊆ 𝐴) → (𝑦 ∈ (𝐴𝐵) → (𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵))))
139, 10, 12sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝑓:𝐴1-1-onto𝑥 → (𝑦 ∈ (𝐴𝐵) → (𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵))))
14 dff1o3 6790 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝐴1-1-onto𝑥 ↔ (𝑓:𝐴onto𝑥 ∧ Fun 𝑓))
15 imadif 6585 . . . . . . . . . . . . . . . . . . . . 21 (Fun 𝑓 → (𝑓 “ (𝐴𝐵)) = ((𝑓𝐴) ∖ (𝑓𝐵)))
1614, 15simplbiim 505 . . . . . . . . . . . . . . . . . . . 20 (𝑓:𝐴1-1-onto𝑥 → (𝑓 “ (𝐴𝐵)) = ((𝑓𝐴) ∖ (𝑓𝐵)))
1716eleq2d 2823 . . . . . . . . . . . . . . . . . . 19 (𝑓:𝐴1-1-onto𝑥 → ((𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵)) ↔ (𝑓𝑦) ∈ ((𝑓𝐴) ∖ (𝑓𝐵))))
1813, 17sylibd 238 . . . . . . . . . . . . . . . . . 18 (𝑓:𝐴1-1-onto𝑥 → (𝑦 ∈ (𝐴𝐵) → (𝑓𝑦) ∈ ((𝑓𝐴) ∖ (𝑓𝐵))))
19 n0i 4293 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑦) ∈ ((𝑓𝐴) ∖ (𝑓𝐵)) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
2018, 19syl6 35 . . . . . . . . . . . . . . . . 17 (𝑓:𝐴1-1-onto𝑥 → (𝑦 ∈ (𝐴𝐵) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅))
218, 20biimtrrid 242 . . . . . . . . . . . . . . . 16 (𝑓:𝐴1-1-onto𝑥 → ((𝑦𝐴 ∧ ¬ 𝑦𝐵) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅))
2221exlimdv 1936 . . . . . . . . . . . . . . 15 (𝑓:𝐴1-1-onto𝑥 → (∃𝑦(𝑦𝐴 ∧ ¬ 𝑦𝐵) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅))
2322imp 407 . . . . . . . . . . . . . 14 ((𝑓:𝐴1-1-onto𝑥 ∧ ∃𝑦(𝑦𝐴 ∧ ¬ 𝑦𝐵)) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
247, 23sylan2 593 . . . . . . . . . . . . 13 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
25 ssdif0 4323 . . . . . . . . . . . . 13 ((𝑓𝐴) ⊆ (𝑓𝐵) ↔ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
2624, 25sylnibr 328 . . . . . . . . . . . 12 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → ¬ (𝑓𝐴) ⊆ (𝑓𝐵))
27 dfpss3 4046 . . . . . . . . . . . 12 ((𝑓𝐵) ⊊ (𝑓𝐴) ↔ ((𝑓𝐵) ⊆ (𝑓𝐴) ∧ ¬ (𝑓𝐴) ⊆ (𝑓𝐵)))
286, 26, 27sylanbrc 583 . . . . . . . . . . 11 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵) ⊊ (𝑓𝐴))
29 imadmrn 6023 . . . . . . . . . . . . . 14 (𝑓 “ dom 𝑓) = ran 𝑓
30 f1odm 6788 . . . . . . . . . . . . . . 15 (𝑓:𝐴1-1-onto𝑥 → dom 𝑓 = 𝐴)
3130imaeq2d 6013 . . . . . . . . . . . . . 14 (𝑓:𝐴1-1-onto𝑥 → (𝑓 “ dom 𝑓) = (𝑓𝐴))
32 f1ofo 6791 . . . . . . . . . . . . . . 15 (𝑓:𝐴1-1-onto𝑥𝑓:𝐴onto𝑥)
33 forn 6759 . . . . . . . . . . . . . . 15 (𝑓:𝐴onto𝑥 → ran 𝑓 = 𝑥)
3432, 33syl 17 . . . . . . . . . . . . . 14 (𝑓:𝐴1-1-onto𝑥 → ran 𝑓 = 𝑥)
3529, 31, 343eqtr3a 2800 . . . . . . . . . . . . 13 (𝑓:𝐴1-1-onto𝑥 → (𝑓𝐴) = 𝑥)
3635psseq2d 4053 . . . . . . . . . . . 12 (𝑓:𝐴1-1-onto𝑥 → ((𝑓𝐵) ⊊ (𝑓𝐴) ↔ (𝑓𝐵) ⊊ 𝑥))
3736adantr 481 . . . . . . . . . . 11 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → ((𝑓𝐵) ⊊ (𝑓𝐴) ↔ (𝑓𝐵) ⊊ 𝑥))
3828, 37mpbid 231 . . . . . . . . . 10 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵) ⊊ 𝑥)
39 php2 9155 . . . . . . . . . 10 ((𝑥 ∈ ω ∧ (𝑓𝐵) ⊊ 𝑥) → (𝑓𝐵) ≺ 𝑥)
4038, 39sylan2 593 . . . . . . . . 9 ((𝑥 ∈ ω ∧ (𝑓:𝐴1-1-onto𝑥𝐵𝐴)) → (𝑓𝐵) ≺ 𝑥)
41 nnfi 9111 . . . . . . . . . 10 (𝑥 ∈ ω → 𝑥 ∈ Fin)
42 f1of1 6783 . . . . . . . . . . . 12 (𝑓:𝐴1-1-onto𝑥𝑓:𝐴1-1𝑥)
43 f1ores 6798 . . . . . . . . . . . 12 ((𝑓:𝐴1-1𝑥𝐵𝐴) → (𝑓𝐵):𝐵1-1-onto→(𝑓𝐵))
4442, 3, 43syl2an 596 . . . . . . . . . . 11 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵):𝐵1-1-onto→(𝑓𝐵))
45 vex 3449 . . . . . . . . . . . . . 14 𝑓 ∈ V
4645resex 5985 . . . . . . . . . . . . 13 (𝑓𝐵) ∈ V
47 f1oeq1 6772 . . . . . . . . . . . . 13 (𝑦 = (𝑓𝐵) → (𝑦:𝐵1-1-onto→(𝑓𝐵) ↔ (𝑓𝐵):𝐵1-1-onto→(𝑓𝐵)))
4846, 47spcev 3565 . . . . . . . . . . . 12 ((𝑓𝐵):𝐵1-1-onto→(𝑓𝐵) → ∃𝑦 𝑦:𝐵1-1-onto→(𝑓𝐵))
49 bren 8893 . . . . . . . . . . . 12 (𝐵 ≈ (𝑓𝐵) ↔ ∃𝑦 𝑦:𝐵1-1-onto→(𝑓𝐵))
5048, 49sylibr 233 . . . . . . . . . . 11 ((𝑓𝐵):𝐵1-1-onto→(𝑓𝐵) → 𝐵 ≈ (𝑓𝐵))
5144, 50syl 17 . . . . . . . . . 10 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → 𝐵 ≈ (𝑓𝐵))
52 endom 8919 . . . . . . . . . . . 12 (𝐵 ≈ (𝑓𝐵) → 𝐵 ≼ (𝑓𝐵))
53 sdomdom 8920 . . . . . . . . . . . . . . 15 ((𝑓𝐵) ≺ 𝑥 → (𝑓𝐵) ≼ 𝑥)
54 domfi 9136 . . . . . . . . . . . . . . 15 ((𝑥 ∈ Fin ∧ (𝑓𝐵) ≼ 𝑥) → (𝑓𝐵) ∈ Fin)
5553, 54sylan2 593 . . . . . . . . . . . . . 14 ((𝑥 ∈ Fin ∧ (𝑓𝐵) ≺ 𝑥) → (𝑓𝐵) ∈ Fin)
56553adant2 1131 . . . . . . . . . . . . 13 ((𝑥 ∈ Fin ∧ 𝐵 ≼ (𝑓𝐵) ∧ (𝑓𝐵) ≺ 𝑥) → (𝑓𝐵) ∈ Fin)
57 domfi 9136 . . . . . . . . . . . . . . 15 (((𝑓𝐵) ∈ Fin ∧ 𝐵 ≼ (𝑓𝐵)) → 𝐵 ∈ Fin)
58573adant3 1132 . . . . . . . . . . . . . 14 (((𝑓𝐵) ∈ Fin ∧ 𝐵 ≼ (𝑓𝐵) ∧ (𝑓𝐵) ≺ 𝑥) → 𝐵 ∈ Fin)
59 domsdomtrfi 9149 . . . . . . . . . . . . . 14 ((𝐵 ∈ Fin ∧ 𝐵 ≼ (𝑓𝐵) ∧ (𝑓𝐵) ≺ 𝑥) → 𝐵𝑥)
6058, 59syld3an1 1410 . . . . . . . . . . . . 13 (((𝑓𝐵) ∈ Fin ∧ 𝐵 ≼ (𝑓𝐵) ∧ (𝑓𝐵) ≺ 𝑥) → 𝐵𝑥)
6156, 60syld3an1 1410 . . . . . . . . . . . 12 ((𝑥 ∈ Fin ∧ 𝐵 ≼ (𝑓𝐵) ∧ (𝑓𝐵) ≺ 𝑥) → 𝐵𝑥)
6252, 61syl3an2 1164 . . . . . . . . . . 11 ((𝑥 ∈ Fin ∧ 𝐵 ≈ (𝑓𝐵) ∧ (𝑓𝐵) ≺ 𝑥) → 𝐵𝑥)
63623expia 1121 . . . . . . . . . 10 ((𝑥 ∈ Fin ∧ 𝐵 ≈ (𝑓𝐵)) → ((𝑓𝐵) ≺ 𝑥𝐵𝑥))
6441, 51, 63syl2an 596 . . . . . . . . 9 ((𝑥 ∈ ω ∧ (𝑓:𝐴1-1-onto𝑥𝐵𝐴)) → ((𝑓𝐵) ≺ 𝑥𝐵𝑥))
6540, 64mpd 15 . . . . . . . 8 ((𝑥 ∈ ω ∧ (𝑓:𝐴1-1-onto𝑥𝐵𝐴)) → 𝐵𝑥)
6665exp32 421 . . . . . . 7 (𝑥 ∈ ω → (𝑓:𝐴1-1-onto𝑥 → (𝐵𝐴𝐵𝑥)))
6766exlimdv 1936 . . . . . 6 (𝑥 ∈ ω → (∃𝑓 𝑓:𝐴1-1-onto𝑥 → (𝐵𝐴𝐵𝑥)))
682, 67biimtrid 241 . . . . 5 (𝑥 ∈ ω → (𝐴𝑥 → (𝐵𝐴𝐵𝑥)))
69 ensymfib 9131 . . . . . . . . . . 11 (𝑥 ∈ Fin → (𝑥𝐴𝐴𝑥))
7069adantr 481 . . . . . . . . . 10 ((𝑥 ∈ Fin ∧ 𝐵𝑥) → (𝑥𝐴𝐴𝑥))
7170biimp3ar 1470 . . . . . . . . 9 ((𝑥 ∈ Fin ∧ 𝐵𝑥𝐴𝑥) → 𝑥𝐴)
72 endom 8919 . . . . . . . . . 10 (𝑥𝐴𝑥𝐴)
73 sdomdom 8920 . . . . . . . . . . . . 13 (𝐵𝑥𝐵𝑥)
74 domfi 9136 . . . . . . . . . . . . 13 ((𝑥 ∈ Fin ∧ 𝐵𝑥) → 𝐵 ∈ Fin)
7573, 74sylan2 593 . . . . . . . . . . . 12 ((𝑥 ∈ Fin ∧ 𝐵𝑥) → 𝐵 ∈ Fin)
76753adant3 1132 . . . . . . . . . . 11 ((𝑥 ∈ Fin ∧ 𝐵𝑥𝑥𝐴) → 𝐵 ∈ Fin)
77 sdomdomtrfi 9148 . . . . . . . . . . 11 ((𝐵 ∈ Fin ∧ 𝐵𝑥𝑥𝐴) → 𝐵𝐴)
7876, 77syld3an1 1410 . . . . . . . . . 10 ((𝑥 ∈ Fin ∧ 𝐵𝑥𝑥𝐴) → 𝐵𝐴)
7972, 78syl3an3 1165 . . . . . . . . 9 ((𝑥 ∈ Fin ∧ 𝐵𝑥𝑥𝐴) → 𝐵𝐴)
8071, 79syld3an3 1409 . . . . . . . 8 ((𝑥 ∈ Fin ∧ 𝐵𝑥𝐴𝑥) → 𝐵𝐴)
8141, 80syl3an1 1163 . . . . . . 7 ((𝑥 ∈ ω ∧ 𝐵𝑥𝐴𝑥) → 𝐵𝐴)
82813com23 1126 . . . . . 6 ((𝑥 ∈ ω ∧ 𝐴𝑥𝐵𝑥) → 𝐵𝐴)
83823exp 1119 . . . . 5 (𝑥 ∈ ω → (𝐴𝑥 → (𝐵𝑥𝐵𝐴)))
8468, 83syldd 72 . . . 4 (𝑥 ∈ ω → (𝐴𝑥 → (𝐵𝐴𝐵𝐴)))
8584rexlimiv 3145 . . 3 (∃𝑥 ∈ ω 𝐴𝑥 → (𝐵𝐴𝐵𝐴))
861, 85sylbi 216 . 2 (𝐴 ∈ Fin → (𝐵𝐴𝐵𝐴))
8786imp 407 1 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  wrex 3073  cdif 3907  wss 3910  wpss 3911  c0 4282   class class class wbr 5105  ccnv 5632  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  Fun wfun 6490   Fn wfn 6491  1-1wf1 6493  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496  ωcom 7802  cen 8880  cdom 8881  csdm 8882  Fincfn 8883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-om 7803  df-1o 8412  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887
This theorem is referenced by:  phpeqd  9159  phpeqdOLD  9169  onomeneq  9172  pssinf  9200  f1finf1o  9215  f1finf1oOLD  9216  findcard3  9229  findcard3OLD  9230  fofinf1o  9271  ackbij1b  10175  fincssdom  10259  fin23lem25  10260  canthp1lem2  10589  pwfseqlem4  10598  uzindi  13887  symggen  19252  pgpssslw  19396  pgpfaclem2  19861  ppiltx  26526  finminlem  34790  lindsenlbs  36073
  Copyright terms: Public domain W3C validator