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

Theorem php3 9271
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 5386. (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 9032 . . 3 (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴𝑥)
2 bren 9009 . . . . . 6 (𝐴𝑥 ↔ ∃𝑓 𝑓:𝐴1-1-onto𝑥)
3 pssss 4115 . . . . . . . . . . . . . 14 (𝐵𝐴𝐵𝐴)
4 imass2 6131 . . . . . . . . . . . . . 14 (𝐵𝐴 → (𝑓𝐵) ⊆ (𝑓𝐴))
53, 4syl 17 . . . . . . . . . . . . 13 (𝐵𝐴 → (𝑓𝐵) ⊆ (𝑓𝐴))
65adantl 481 . . . . . . . . . . . 12 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵) ⊆ (𝑓𝐴))
7 pssnel 4490 . . . . . . . . . . . . . 14 (𝐵𝐴 → ∃𝑦(𝑦𝐴 ∧ ¬ 𝑦𝐵))
8 eldif 3980 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴 ∧ ¬ 𝑦𝐵))
9 f1ofn 6862 . . . . . . . . . . . . . . . . . . . 20 (𝑓:𝐴1-1-onto𝑥𝑓 Fn 𝐴)
10 difss 4153 . . . . . . . . . . . . . . . . . . . 20 (𝐴𝐵) ⊆ 𝐴
11 fnfvima 7268 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 Fn 𝐴 ∧ (𝐴𝐵) ⊆ 𝐴𝑦 ∈ (𝐴𝐵)) → (𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵)))
12113expia 1121 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 Fn 𝐴 ∧ (𝐴𝐵) ⊆ 𝐴) → (𝑦 ∈ (𝐴𝐵) → (𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵))))
139, 10, 12sylancl 585 . . . . . . . . . . . . . . . . . . 19 (𝑓:𝐴1-1-onto𝑥 → (𝑦 ∈ (𝐴𝐵) → (𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵))))
14 dff1o3 6867 . . . . . . . . . . . . . . . . . . . . 21 (𝑓:𝐴1-1-onto𝑥 ↔ (𝑓:𝐴onto𝑥 ∧ Fun 𝑓))
15 imadif 6661 . . . . . . . . . . . . . . . . . . . . 21 (Fun 𝑓 → (𝑓 “ (𝐴𝐵)) = ((𝑓𝐴) ∖ (𝑓𝐵)))
1614, 15simplbiim 504 . . . . . . . . . . . . . . . . . . . 20 (𝑓:𝐴1-1-onto𝑥 → (𝑓 “ (𝐴𝐵)) = ((𝑓𝐴) ∖ (𝑓𝐵)))
1716eleq2d 2824 . . . . . . . . . . . . . . . . . . 19 (𝑓:𝐴1-1-onto𝑥 → ((𝑓𝑦) ∈ (𝑓 “ (𝐴𝐵)) ↔ (𝑓𝑦) ∈ ((𝑓𝐴) ∖ (𝑓𝐵))))
1813, 17sylibd 239 . . . . . . . . . . . . . . . . . 18 (𝑓:𝐴1-1-onto𝑥 → (𝑦 ∈ (𝐴𝐵) → (𝑓𝑦) ∈ ((𝑓𝐴) ∖ (𝑓𝐵))))
19 n0i 4358 . . . . . . . . . . . . . . . . . 18 ((𝑓𝑦) ∈ ((𝑓𝐴) ∖ (𝑓𝐵)) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
2018, 19syl6 35 . . . . . . . . . . . . . . . . 17 (𝑓:𝐴1-1-onto𝑥 → (𝑦 ∈ (𝐴𝐵) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅))
218, 20biimtrrid 243 . . . . . . . . . . . . . . . 16 (𝑓:𝐴1-1-onto𝑥 → ((𝑦𝐴 ∧ ¬ 𝑦𝐵) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅))
2221exlimdv 1932 . . . . . . . . . . . . . . 15 (𝑓:𝐴1-1-onto𝑥 → (∃𝑦(𝑦𝐴 ∧ ¬ 𝑦𝐵) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅))
2322imp 406 . . . . . . . . . . . . . 14 ((𝑓:𝐴1-1-onto𝑥 ∧ ∃𝑦(𝑦𝐴 ∧ ¬ 𝑦𝐵)) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
247, 23sylan2 592 . . . . . . . . . . . . 13 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → ¬ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
25 ssdif0 4384 . . . . . . . . . . . . 13 ((𝑓𝐴) ⊆ (𝑓𝐵) ↔ ((𝑓𝐴) ∖ (𝑓𝐵)) = ∅)
2624, 25sylnibr 329 . . . . . . . . . . . 12 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → ¬ (𝑓𝐴) ⊆ (𝑓𝐵))
27 dfpss3 4106 . . . . . . . . . . . 12 ((𝑓𝐵) ⊊ (𝑓𝐴) ↔ ((𝑓𝐵) ⊆ (𝑓𝐴) ∧ ¬ (𝑓𝐴) ⊆ (𝑓𝐵)))
286, 26, 27sylanbrc 582 . . . . . . . . . . 11 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵) ⊊ (𝑓𝐴))
29 imadmrn 6098 . . . . . . . . . . . . . 14 (𝑓 “ dom 𝑓) = ran 𝑓
30 f1odm 6865 . . . . . . . . . . . . . . 15 (𝑓:𝐴1-1-onto𝑥 → dom 𝑓 = 𝐴)
3130imaeq2d 6088 . . . . . . . . . . . . . 14 (𝑓:𝐴1-1-onto𝑥 → (𝑓 “ dom 𝑓) = (𝑓𝐴))
32 f1ofo 6868 . . . . . . . . . . . . . . 15 (𝑓:𝐴1-1-onto𝑥𝑓:𝐴onto𝑥)
33 forn 6836 . . . . . . . . . . . . . . 15 (𝑓:𝐴onto𝑥 → ran 𝑓 = 𝑥)
3432, 33syl 17 . . . . . . . . . . . . . 14 (𝑓:𝐴1-1-onto𝑥 → ran 𝑓 = 𝑥)
3529, 31, 343eqtr3a 2798 . . . . . . . . . . . . 13 (𝑓:𝐴1-1-onto𝑥 → (𝑓𝐴) = 𝑥)
3635psseq2d 4113 . . . . . . . . . . . 12 (𝑓:𝐴1-1-onto𝑥 → ((𝑓𝐵) ⊊ (𝑓𝐴) ↔ (𝑓𝐵) ⊊ 𝑥))
3736adantr 480 . . . . . . . . . . 11 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → ((𝑓𝐵) ⊊ (𝑓𝐴) ↔ (𝑓𝐵) ⊊ 𝑥))
3828, 37mpbid 232 . . . . . . . . . 10 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵) ⊊ 𝑥)
39 php2 9270 . . . . . . . . . 10 ((𝑥 ∈ ω ∧ (𝑓𝐵) ⊊ 𝑥) → (𝑓𝐵) ≺ 𝑥)
4038, 39sylan2 592 . . . . . . . . 9 ((𝑥 ∈ ω ∧ (𝑓:𝐴1-1-onto𝑥𝐵𝐴)) → (𝑓𝐵) ≺ 𝑥)
41 nnfi 9229 . . . . . . . . . 10 (𝑥 ∈ ω → 𝑥 ∈ Fin)
42 f1of1 6860 . . . . . . . . . . . 12 (𝑓:𝐴1-1-onto𝑥𝑓:𝐴1-1𝑥)
43 f1ores 6875 . . . . . . . . . . . 12 ((𝑓:𝐴1-1𝑥𝐵𝐴) → (𝑓𝐵):𝐵1-1-onto→(𝑓𝐵))
4442, 3, 43syl2an 595 . . . . . . . . . . 11 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → (𝑓𝐵):𝐵1-1-onto→(𝑓𝐵))
45 vex 3486 . . . . . . . . . . . . . 14 𝑓 ∈ V
4645resex 6057 . . . . . . . . . . . . 13 (𝑓𝐵) ∈ V
47 f1oeq1 6849 . . . . . . . . . . . . 13 (𝑦 = (𝑓𝐵) → (𝑦:𝐵1-1-onto→(𝑓𝐵) ↔ (𝑓𝐵):𝐵1-1-onto→(𝑓𝐵)))
4846, 47spcev 3615 . . . . . . . . . . . 12 ((𝑓𝐵):𝐵1-1-onto→(𝑓𝐵) → ∃𝑦 𝑦:𝐵1-1-onto→(𝑓𝐵))
49 bren 9009 . . . . . . . . . . . 12 (𝐵 ≈ (𝑓𝐵) ↔ ∃𝑦 𝑦:𝐵1-1-onto→(𝑓𝐵))
5048, 49sylibr 234 . . . . . . . . . . 11 ((𝑓𝐵):𝐵1-1-onto→(𝑓𝐵) → 𝐵 ≈ (𝑓𝐵))
5144, 50syl 17 . . . . . . . . . 10 ((𝑓:𝐴1-1-onto𝑥𝐵𝐴) → 𝐵 ≈ (𝑓𝐵))
52 endom 9035 . . . . . . . . . . . 12 (𝐵 ≈ (𝑓𝐵) → 𝐵 ≼ (𝑓𝐵))
53 sdomdom 9036 . . . . . . . . . . . . . . 15 ((𝑓𝐵) ≺ 𝑥 → (𝑓𝐵) ≼ 𝑥)
54 domfi 9251 . . . . . . . . . . . . . . 15 ((𝑥 ∈ Fin ∧ (𝑓𝐵) ≼ 𝑥) → (𝑓𝐵) ∈ Fin)
5553, 54sylan2 592 . . . . . . . . . . . . . 14 ((𝑥 ∈ Fin ∧ (𝑓𝐵) ≺ 𝑥) → (𝑓𝐵) ∈ Fin)
56553adant2 1131 . . . . . . . . . . . . 13 ((𝑥 ∈ Fin ∧ 𝐵 ≼ (𝑓𝐵) ∧ (𝑓𝐵) ≺ 𝑥) → (𝑓𝐵) ∈ Fin)
57 domfi 9251 . . . . . . . . . . . . . . 15 (((𝑓𝐵) ∈ Fin ∧ 𝐵 ≼ (𝑓𝐵)) → 𝐵 ∈ Fin)
58573adant3 1132 . . . . . . . . . . . . . 14 (((𝑓𝐵) ∈ Fin ∧ 𝐵 ≼ (𝑓𝐵) ∧ (𝑓𝐵) ≺ 𝑥) → 𝐵 ∈ Fin)
59 domsdomtrfi 9264 . . . . . . . . . . . . . 14 ((𝐵 ∈ Fin ∧ 𝐵 ≼ (𝑓𝐵) ∧ (𝑓𝐵) ≺ 𝑥) → 𝐵𝑥)
6058, 59syld3an1 1410 . . . . . . . . . . . . 13 (((𝑓𝐵) ∈ Fin ∧ 𝐵 ≼ (𝑓𝐵) ∧ (𝑓𝐵) ≺ 𝑥) → 𝐵𝑥)
6156, 60syld3an1 1410 . . . . . . . . . . . 12 ((𝑥 ∈ Fin ∧ 𝐵 ≼ (𝑓𝐵) ∧ (𝑓𝐵) ≺ 𝑥) → 𝐵𝑥)
6252, 61syl3an2 1164 . . . . . . . . . . 11 ((𝑥 ∈ Fin ∧ 𝐵 ≈ (𝑓𝐵) ∧ (𝑓𝐵) ≺ 𝑥) → 𝐵𝑥)
63623expia 1121 . . . . . . . . . 10 ((𝑥 ∈ Fin ∧ 𝐵 ≈ (𝑓𝐵)) → ((𝑓𝐵) ≺ 𝑥𝐵𝑥))
6441, 51, 63syl2an 595 . . . . . . . . 9 ((𝑥 ∈ ω ∧ (𝑓:𝐴1-1-onto𝑥𝐵𝐴)) → ((𝑓𝐵) ≺ 𝑥𝐵𝑥))
6540, 64mpd 15 . . . . . . . 8 ((𝑥 ∈ ω ∧ (𝑓:𝐴1-1-onto𝑥𝐵𝐴)) → 𝐵𝑥)
6665exp32 420 . . . . . . 7 (𝑥 ∈ ω → (𝑓:𝐴1-1-onto𝑥 → (𝐵𝐴𝐵𝑥)))
6766exlimdv 1932 . . . . . 6 (𝑥 ∈ ω → (∃𝑓 𝑓:𝐴1-1-onto𝑥 → (𝐵𝐴𝐵𝑥)))
682, 67biimtrid 242 . . . . 5 (𝑥 ∈ ω → (𝐴𝑥 → (𝐵𝐴𝐵𝑥)))
69 ensymfib 9246 . . . . . . . . . . 11 (𝑥 ∈ Fin → (𝑥𝐴𝐴𝑥))
7069adantr 480 . . . . . . . . . 10 ((𝑥 ∈ Fin ∧ 𝐵𝑥) → (𝑥𝐴𝐴𝑥))
7170biimp3ar 1470 . . . . . . . . 9 ((𝑥 ∈ Fin ∧ 𝐵𝑥𝐴𝑥) → 𝑥𝐴)
72 endom 9035 . . . . . . . . . 10 (𝑥𝐴𝑥𝐴)
73 sdomdom 9036 . . . . . . . . . . . . 13 (𝐵𝑥𝐵𝑥)
74 domfi 9251 . . . . . . . . . . . . 13 ((𝑥 ∈ Fin ∧ 𝐵𝑥) → 𝐵 ∈ Fin)
7573, 74sylan2 592 . . . . . . . . . . . 12 ((𝑥 ∈ Fin ∧ 𝐵𝑥) → 𝐵 ∈ Fin)
76753adant3 1132 . . . . . . . . . . 11 ((𝑥 ∈ Fin ∧ 𝐵𝑥𝑥𝐴) → 𝐵 ∈ Fin)
77 sdomdomtrfi 9263 . . . . . . . . . . 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 3150 . . 3 (∃𝑥 ∈ ω 𝐴𝑥 → (𝐵𝐴𝐵𝐴))
861, 85sylbi 217 . 2 (𝐴 ∈ Fin → (𝐵𝐴𝐵𝐴))
8786imp 406 1 ((𝐴 ∈ Fin ∧ 𝐵𝐴) → 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1537  wex 1777  wcel 2103  wrex 3072  cdif 3967  wss 3970  wpss 3971  c0 4347   class class class wbr 5169  ccnv 5698  dom cdm 5699  ran crn 5700  cres 5701  cima 5702  Fun wfun 6566   Fn wfn 6567  1-1wf1 6569  ontowfo 6570  1-1-ontowf1o 6571  cfv 6572  ωcom 7899  cen 8996  cdom 8997  csdm 8998  Fincfn 8999
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pr 5450  ax-un 7766
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-ral 3064  df-rex 3073  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-pss 3990  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5170  df-opab 5232  df-mpt 5253  df-tr 5287  df-id 5597  df-eprel 5603  df-po 5611  df-so 5612  df-fr 5654  df-we 5656  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-ord 6397  df-on 6398  df-lim 6399  df-suc 6400  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-f1 6577  df-fo 6578  df-f1o 6579  df-fv 6580  df-om 7900  df-1o 8518  df-en 9000  df-dom 9001  df-sdom 9002  df-fin 9003
This theorem is referenced by:  phpeqd  9274  phpeqdOLD  9284  onomeneq  9287  pssinf  9315  f1finf1o  9329  f1finf1oOLD  9330  findcard3  9342  findcard3OLD  9343  fofinf1o  9396  ackbij1b  10303  fincssdom  10388  fin23lem25  10389  canthp1lem2  10718  pwfseqlem4  10727  uzindi  14029  symggen  19507  pgpssslw  19651  pgpfaclem2  20121  ppiltx  27229  finminlem  36231  lindsenlbs  37523
  Copyright terms: Public domain W3C validator