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 
|- A e. _V
Assertion phplem2 
|- ( ( A e. _om /\ B e. _om ) -> ( suc A ~~ suc B -> A ~~ B ) )

Proof

Step Hyp Ref Expression
1 phplem2.1 
 |-  A e. _V
2 bren 
 |-  ( suc A ~~ suc B <-> E. f f : suc A -1-1-onto-> suc B )
3 f1of1 
 |-  ( f : suc A -1-1-onto-> suc B -> f : suc A -1-1-> suc B )
4 nnfi 
 |-  ( A e. _om -> A e. Fin )
5 sssucid 
 |-  A C_ suc A
6 f1imaenfi 
 |-  ( ( f : suc A -1-1-> suc B /\ A C_ suc A /\ A e. Fin ) -> ( f " A ) ~~ A )
7 5 6 mp3an2 
 |-  ( ( f : suc A -1-1-> suc B /\ A e. Fin ) -> ( f " A ) ~~ A )
8 3 4 7 syl2anr 
 |-  ( ( A e. _om /\ f : suc A -1-1-onto-> suc B ) -> ( f " A ) ~~ A )
9 ensymfib 
 |-  ( A e. Fin -> ( A ~~ ( f " A ) <-> ( f " A ) ~~ A ) )
10 4 9 syl 
 |-  ( A e. _om -> ( A ~~ ( f " A ) <-> ( f " A ) ~~ A ) )
11 10 adantr 
 |-  ( ( A e. _om /\ f : suc A -1-1-onto-> suc B ) -> ( A ~~ ( f " A ) <-> ( f " A ) ~~ A ) )
12 8 11 mpbird 
 |-  ( ( A e. _om /\ f : suc A -1-1-onto-> suc B ) -> A ~~ ( f " A ) )
13 nnord 
 |-  ( A e. _om -> Ord A )
14 orddif 
 |-  ( Ord A -> A = ( suc A \ { A } ) )
15 13 14 syl 
 |-  ( A e. _om -> A = ( suc A \ { A } ) )
16 15 imaeq2d 
 |-  ( A e. _om -> ( f " A ) = ( f " ( suc A \ { A } ) ) )
17 f1ofn 
 |-  ( f : suc A -1-1-onto-> suc B -> f Fn suc A )
18 1 sucid 
 |-  A e. suc A
19 fnsnfv 
 |-  ( ( f Fn suc A /\ A e. suc A ) -> { ( f ` A ) } = ( f " { A } ) )
20 17 18 19 sylancl 
 |-  ( f : suc A -1-1-onto-> suc B -> { ( f ` A ) } = ( f " { A } ) )
21 20 difeq2d 
 |-  ( f : suc A -1-1-onto-> suc B -> ( ( f " suc A ) \ { ( f ` A ) } ) = ( ( f " suc A ) \ ( f " { A } ) ) )
22 imadmrn 
 |-  ( f " dom f ) = ran f
23 22 eqcomi 
 |-  ran f = ( f " dom f )
24 f1ofo 
 |-  ( f : suc A -1-1-onto-> suc B -> f : suc A -onto-> suc B )
25 forn 
 |-  ( f : suc A -onto-> suc B -> ran f = suc B )
26 24 25 syl 
 |-  ( f : suc A -1-1-onto-> suc B -> ran f = suc B )
27 f1odm 
 |-  ( f : suc A -1-1-onto-> suc B -> dom f = suc A )
28 27 imaeq2d 
 |-  ( f : suc A -1-1-onto-> suc B -> ( f " dom f ) = ( f " suc A ) )
29 23 26 28 3eqtr3a 
 |-  ( f : suc A -1-1-onto-> suc B -> suc B = ( f " suc A ) )
30 29 difeq1d 
 |-  ( f : suc A -1-1-onto-> suc B -> ( suc B \ { ( f ` A ) } ) = ( ( f " suc A ) \ { ( f ` A ) } ) )
31 dff1o3 
 |-  ( f : suc A -1-1-onto-> suc B <-> ( f : suc A -onto-> suc B /\ Fun `' f ) )
32 imadif 
 |-  ( Fun `' f -> ( f " ( suc A \ { A } ) ) = ( ( f " suc A ) \ ( f " { A } ) ) )
33 31 32 simplbiim 
 |-  ( f : suc A -1-1-onto-> suc B -> ( f " ( suc A \ { A } ) ) = ( ( f " suc A ) \ ( f " { A } ) ) )
34 21 30 33 3eqtr4rd 
 |-  ( f : suc A -1-1-onto-> suc B -> ( f " ( suc A \ { A } ) ) = ( suc B \ { ( f ` A ) } ) )
35 16 34 sylan9eq 
 |-  ( ( A e. _om /\ f : suc A -1-1-onto-> suc B ) -> ( f " A ) = ( suc B \ { ( f ` A ) } ) )
36 12 35 breqtrd 
 |-  ( ( A e. _om /\ f : suc A -1-1-onto-> suc B ) -> A ~~ ( suc B \ { ( f ` A ) } ) )
37 fnfvelrn 
 |-  ( ( f Fn suc A /\ A e. suc A ) -> ( f ` A ) e. ran f )
38 17 18 37 sylancl 
 |-  ( f : suc A -1-1-onto-> suc B -> ( f ` A ) e. ran f )
39 25 eleq2d 
 |-  ( f : suc A -onto-> suc B -> ( ( f ` A ) e. ran f <-> ( f ` A ) e. suc B ) )
40 24 39 syl 
 |-  ( f : suc A -1-1-onto-> suc B -> ( ( f ` A ) e. ran f <-> ( f ` A ) e. suc B ) )
41 38 40 mpbid 
 |-  ( f : suc A -1-1-onto-> suc B -> ( f ` A ) e. suc B )
42 phplem1 
 |-  ( ( B e. _om /\ ( f ` A ) e. suc B ) -> B ~~ ( suc B \ { ( f ` A ) } ) )
43 41 42 sylan2 
 |-  ( ( B e. _om /\ f : suc A -1-1-onto-> suc B ) -> B ~~ ( suc B \ { ( f ` A ) } ) )
44 nnfi 
 |-  ( B e. _om -> B e. Fin )
45 ensymfib 
 |-  ( B e. Fin -> ( B ~~ ( suc B \ { ( f ` A ) } ) <-> ( suc B \ { ( f ` A ) } ) ~~ B ) )
46 44 45 syl 
 |-  ( B e. _om -> ( B ~~ ( suc B \ { ( f ` A ) } ) <-> ( suc B \ { ( f ` A ) } ) ~~ B ) )
47 46 adantr 
 |-  ( ( B e. _om /\ f : suc A -1-1-onto-> suc B ) -> ( B ~~ ( suc B \ { ( f ` A ) } ) <-> ( suc B \ { ( f ` A ) } ) ~~ B ) )
48 43 47 mpbid 
 |-  ( ( B e. _om /\ f : suc A -1-1-onto-> suc B ) -> ( suc B \ { ( f ` A ) } ) ~~ B )
49 entrfil 
 |-  ( ( A e. Fin /\ A ~~ ( suc B \ { ( f ` A ) } ) /\ ( suc B \ { ( f ` A ) } ) ~~ B ) -> A ~~ B )
50 4 49 syl3an1 
 |-  ( ( A e. _om /\ A ~~ ( suc B \ { ( f ` A ) } ) /\ ( suc B \ { ( f ` A ) } ) ~~ B ) -> A ~~ B )
51 48 50 syl3an3 
 |-  ( ( A e. _om /\ A ~~ ( suc B \ { ( f ` A ) } ) /\ ( B e. _om /\ f : suc A -1-1-onto-> suc B ) ) -> A ~~ B )
52 51 3expa 
 |-  ( ( ( A e. _om /\ A ~~ ( suc B \ { ( f ` A ) } ) ) /\ ( B e. _om /\ f : suc A -1-1-onto-> suc B ) ) -> A ~~ B )
53 36 52 syldanl 
 |-  ( ( ( A e. _om /\ f : suc A -1-1-onto-> suc B ) /\ ( B e. _om /\ f : suc A -1-1-onto-> suc B ) ) -> A ~~ B )
54 53 anandirs 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ f : suc A -1-1-onto-> suc B ) -> A ~~ B )
55 54 ex 
 |-  ( ( A e. _om /\ B e. _om ) -> ( f : suc A -1-1-onto-> suc B -> A ~~ B ) )
56 55 exlimdv 
 |-  ( ( A e. _om /\ B e. _om ) -> ( E. f f : suc A -1-1-onto-> suc B -> A ~~ B ) )
57 2 56 syl5bi 
 |-  ( ( A e. _om /\ B e. _om ) -> ( suc A ~~ suc B -> A ~~ B ) )