Metamath Proof Explorer

Theorem phplem4

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)

Ref Expression
Hypotheses phplem2.1 
|- A e. _V
phplem2.2 
|- B e. _V
Assertion phplem4 
|- ( ( A e. _om /\ B e. _om ) -> ( suc A ~~ suc B -> A ~~ B ) )

Proof

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