Metamath Proof Explorer


Theorem phplem2

Description: Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers. (Contributed by NM, 28-May-1998) (Revised by Mario Carneiro, 24-Jun-2015) Avoid ax-pow . (Revised by BTernaryTau, 4-Nov-2024)

Ref Expression
Hypothesis phplem2.1 AV
Assertion phplem2 AωBωsucAsucBAB

Proof

Step Hyp Ref Expression
1 phplem2.1 AV
2 bren sucAsucBff:sucA1-1 ontosucB
3 f1of1 f:sucA1-1 ontosucBf:sucA1-1sucB
4 nnfi AωAFin
5 sssucid AsucA
6 f1imaenfi f:sucA1-1sucBAsucAAFinfAA
7 5 6 mp3an2 f:sucA1-1sucBAFinfAA
8 3 4 7 syl2anr Aωf:sucA1-1 ontosucBfAA
9 ensymfib AFinAfAfAA
10 4 9 syl AωAfAfAA
11 10 adantr Aωf:sucA1-1 ontosucBAfAfAA
12 8 11 mpbird Aωf:sucA1-1 ontosucBAfA
13 nnord AωOrdA
14 orddif OrdAA=sucAA
15 13 14 syl AωA=sucAA
16 15 imaeq2d AωfA=fsucAA
17 f1ofn f:sucA1-1 ontosucBfFnsucA
18 1 sucid AsucA
19 fnsnfv fFnsucAAsucAfA=fA
20 17 18 19 sylancl f:sucA1-1 ontosucBfA=fA
21 20 difeq2d f:sucA1-1 ontosucBfsucAfA=fsucAfA
22 imadmrn fdomf=ranf
23 22 eqcomi ranf=fdomf
24 f1ofo f:sucA1-1 ontosucBf:sucAontosucB
25 forn f:sucAontosucBranf=sucB
26 24 25 syl f:sucA1-1 ontosucBranf=sucB
27 f1odm f:sucA1-1 ontosucBdomf=sucA
28 27 imaeq2d f:sucA1-1 ontosucBfdomf=fsucA
29 23 26 28 3eqtr3a f:sucA1-1 ontosucBsucB=fsucA
30 29 difeq1d f:sucA1-1 ontosucBsucBfA=fsucAfA
31 dff1o3 f:sucA1-1 ontosucBf:sucAontosucBFunf-1
32 imadif Funf-1fsucAA=fsucAfA
33 31 32 simplbiim f:sucA1-1 ontosucBfsucAA=fsucAfA
34 21 30 33 3eqtr4rd f:sucA1-1 ontosucBfsucAA=sucBfA
35 16 34 sylan9eq Aωf:sucA1-1 ontosucBfA=sucBfA
36 12 35 breqtrd Aωf:sucA1-1 ontosucBAsucBfA
37 fnfvelrn fFnsucAAsucAfAranf
38 17 18 37 sylancl f:sucA1-1 ontosucBfAranf
39 25 eleq2d f:sucAontosucBfAranffAsucB
40 24 39 syl f:sucA1-1 ontosucBfAranffAsucB
41 38 40 mpbid f:sucA1-1 ontosucBfAsucB
42 phplem1 BωfAsucBBsucBfA
43 41 42 sylan2 Bωf:sucA1-1 ontosucBBsucBfA
44 nnfi BωBFin
45 ensymfib BFinBsucBfAsucBfAB
46 44 45 syl BωBsucBfAsucBfAB
47 46 adantr Bωf:sucA1-1 ontosucBBsucBfAsucBfAB
48 43 47 mpbid Bωf:sucA1-1 ontosucBsucBfAB
49 entrfil AFinAsucBfAsucBfABAB
50 4 49 syl3an1 AωAsucBfAsucBfABAB
51 48 50 syl3an3 AωAsucBfABωf:sucA1-1 ontosucBAB
52 51 3expa AωAsucBfABωf:sucA1-1 ontosucBAB
53 36 52 syldanl Aωf:sucA1-1 ontosucBBωf:sucA1-1 ontosucBAB
54 53 anandirs AωBωf:sucA1-1 ontosucBAB
55 54 ex AωBωf:sucA1-1 ontosucBAB
56 55 exlimdv AωBωff:sucA1-1 ontosucBAB
57 2 56 syl5bi AωBωsucAsucBAB