HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem phplem4 4491
Description: Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers.
Hypotheses
Ref Expression
phplem2.1 |- A e. V
phplem2.2 |- B e. V
Assertion
Ref Expression
phplem4 |- ((A e. om /\ B e. om) -> (suc A ~~ suc B -> A ~~ B))
Proof of Theorem phplem4
StepHypRef Expression
1 entrt 4395 . . . . . 6 |- ((A ~~ (suc B \ {(f` A)}) /\ (suc B \ {(f` A)}) ~~ B) -> A ~~ B)
2 f1of1 3673 . . . . . . . . . 10 |- (f:suc A-1-1-onto->suc B -> f:suc A-1-1->suc B)
3 sssucid 3037 . . . . . . . . . 10 |- A (_ suc A
42, 3jctir 293 . . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> (f:suc A-1-1->suc B /\ A (_ suc A))
5 f1ores 3688 . . . . . . . . 9 |- ((f:suc A-1-1->suc B /\ A (_ suc A) -> (f |` A):A-1-1-onto->(f"A))
6 phplem2.1 . . . . . . . . . 10 |- A e. V
76f1oen 4379 . . . . . . . . 9 |- ((f |` A):A-1-1-onto->(f"A) -> A ~~ (f"A))
84, 5, 73syl 20 . . . . . . . 8 |- (f:suc A-1-1-onto->suc B -> A ~~ (f"A))
98adantl 388 . . . . . . 7 |- ((A e. om /\ f:suc A-1-1-onto->suc B) -> A ~~ (f"A))
10 nnord 3130 . . . . . . . . 9 |- (A e. om -> Ord A)
11 orddif 3065 . . . . . . . . 9 |- (Ord A -> A = (suc A \ {A}))
12 imaeq2 3386 . . . . . . . . 9 |- (A = (suc A \ {A}) -> (f"A) = (f"(suc A \ {A})))
1310, 11, 123syl 20 . . . . . . . 8 |- (A e. om -> (f"A) = (f"(suc A \ {A})))
14 f1ofn 3675 . . . . . . . . . 10 |- (f:suc A-1-1-onto->suc B -> f Fn suc A)
156sucid 3041 . . . . . . . . . . 11 |- A e. suc A
16 fnsnfv 3752 . . . . . . . . . . 11 |- ((f Fn suc A /\ A e. suc A) -> {(f` A)} = (f"{A}))
1715, 16mpan2 694 . . . . . . . . . 10 |- (f Fn suc A -> {(f` A)} = (f"{A}))
18 difeq2 2144 . . . . . . . . . 10 |- ({(f` A)} = (f"{A}) -> ((f"suc A) \ {(f` A)}) = ((f"suc A) \ (f"{A})))
1914, 17, 183syl 20 . . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> ((f"suc A) \ {(f` A)}) = ((f"suc A) \ (f"{A})))
20 imadmrn 3398 . . . . . . . . . . . . 13 |- (f"dom f) = ran f
2120eqcomi 1471 . . . . . . . . . . . 12 |- ran f = (f"dom f)
2221a1i 8 . . . . . . . . . . 11 |- (f:suc A-1-1-onto->suc B -> ran f = (f"dom f))
23 f1ofo 3680 . . . . . . . . . . . 12 |- (f:suc A-1-1-onto->suc B -> f:suc A-onto->suc B)
24 forn 3659 . . . . . . . . . . . 12 |- (f:suc A-onto->suc B -> ran f = suc B)
2523, 24syl 10 . . . . . . . . . . 11 |- (f:suc A-1-1-onto->suc B -> ran f = suc B)
26 fndm 3573 . . . . . . . . . . . 12 |- (f Fn suc A -> dom f = suc A)
27 imaeq2 3386 . . . . . . . . . . . 12 |- (dom f = suc A -> (f"dom f) = (f"suc A))
2814, 26, 273syl 20 . . . . . . . . . . 11 |- (f:suc A-1-1-onto->suc B -> (f"dom f) = (f"suc A))
2922, 25, 283eqtr3d 1507 . . . . . . . . . 10 |- (f:suc A-1-1-onto->suc B -> suc B = (f"suc A))
3029difeq1d 2148 . . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> (suc B \ {(f` A)}) = ((f"suc A) \ {(f` A)}))
31 f1o3 3679 . . . . . . . . . . 11 |- (f:suc A-1-1-onto->suc B <-> (f:suc A-onto->suc B /\ Fun `'f))
3231pm3.27bi 326 . . . . . . . . . 10 |- (f:suc A-1-1-onto->suc B -> Fun `'f)
33 imadif 3560 . . . . . . . . . 10 |- (Fun `'f -> (f"(suc A \ {A})) = ((f"suc A) \ (f"{A})))
3432, 33syl 10 . . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> (f"(suc A \ {A})) = ((f"suc A) \ (f"{A})))
3519, 30, 343eqtr4rd 1510 . . . . . . . 8 |- (f:suc A-1-1-onto->suc B -> (f"(suc A \ {A})) = (suc B \ {(f` A)}))
3613, 35sylan9eq 1519 . . . . . . 7 |- ((A e. om /\ f:suc A-1-1-onto->suc B) -> (f"A) = (suc B \ {(f` A)}))
379, 36breqtrd 2629 . . . . . 6 |- ((A e. om /\ f:suc A-1-1-onto->suc B) -> A ~~ (suc B \ {(f` A)}))
38 phplem2.2 . . . . . . . . 9 |- B e. V
39 fvex 3717 . . . . . . . . 9 |- (f` A) e. V
4038, 39phplem3 4490 . . . . . . . 8 |- ((B e. om /\ (f` A) e. suc B) -> B ~~ (suc B \ {(f` A)}))
41 fnfvelrn 3798 . . . . . . . . . . 11 |- ((f Fn suc A /\ A e. suc A) -> (f` A) e. ran f)
4215, 41mpan2 694 . . . . . . . . . 10 |- (f Fn suc A -> (f` A) e. ran f)
4314, 42syl 10 . . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> (f` A) e. ran f)
4424eleq2d 1533 . . . . . . . . . 10 |- (f:suc A-onto->suc B -> ((f` A) e. ran f <-> (f` A) e. suc B))
4523, 44syl 10 . . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> ((f` A) e. ran f <-> (f` A) e. suc B))
4643, 45mpbid 195 . . . . . . . 8 |- (f:suc A-1-1-onto->suc B -> (f` A) e. suc B)
4740, 46sylan2 451 . . . . . . 7 |- ((B e. om /\ f:suc A-1-1-onto->suc B) -> B ~~ (suc B \ {(f` A)}))
4838sucex 3040 . . . . . . . . 9 |- suc B e. V
49 difss 2157 . . . . . . . . 9 |- (suc B \ {(f` A)}) (_ suc B
5048, 49ssexi 2710 . . . . . . . 8 |- (suc B \ {(f` A)}) e. V
5150ensym 4393 . . . . . . 7 |- (B ~~ (suc B \ {(f` A)}) -> (suc B \ {(f` A)}) ~~ B)
5247, 51syl 10 . . . . . 6 |- ((B e. om /\ f:suc A-1-1-onto->suc B) -> (suc B \ {(f` A)}) ~~ B)
531, 37, 52syl2an 454 . . . . 5 |- (((A e. om /\ f:suc A-1-1-onto->suc B) /\ (B e. om /\ f:suc A-1-1-onto->suc B)) -> A ~~ B)
5453anandirs 512 . . . 4 |- (((A e. om /\ B e. om) /\ f:suc A-1-1-onto->suc B) -> A ~~ B)
5554ex 373 . . 3 |- ((A e. om /\ B e. om) -> (f:suc A-1-1-onto->suc B -> A ~~ B))
565519.23adv 1209 . 2 |- ((A e. om /\ B e. om) -> (E.f f:suc A-1-1-onto->suc B -> A ~~ B))
5748bren 4359 . 2 |- (suc A ~~ suc B <-> E.f f:suc A-1-1-onto->suc B)
5856, 57syl5ib 206 1 |- ((A e. om /\ B e. om) -> (suc A ~~ suc B -> A ~~ B))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  E.wex 977  Vcvv 1802   \ cdif 2034   (_ wss 2037  {csn 2399   class class class wbr 2609  Ord word 2937  suc csuc 2940  omcom 3121  `'ccnv 3159  dom cdm 3160  ran crn 3161   |` cres 3162  "cima 3163  Fun wfun 3166   Fn wfn 3167  -1-1->wf1 3169  -onto->wfo 3170  -1-1-onto->wf1o 3171  ` cfv 3172   ~~ cen 4348
This theorem is referenced by:  nneneq 4492
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-id 2824  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942  df-suc 2944  df-om 3122  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-f1 3185  df-fo 3186  df-f1o 3187  df-fv 3188  df-er 4245  df-en 4351
Copyright terms: Public domain