Metamath Proof Explorer

Theorem php3

Description: Corollary of Pigeonhole Principle. If A is finite and B is a proper subset of A , the B is strictly less numerous than A . Stronger version of Corollary 6C of Enderton p. 135. (Contributed by NM, 22-Aug-2008) Avoid ax-pow . (Revised by BTernaryTau, 26-Nov-2024)

Ref Expression
Assertion php3 
|- ( ( A e. Fin /\ B C. A ) -> B ~< A )

Proof

Step Hyp Ref Expression
1 isfi 
 |-  ( A e. Fin <-> E. x e. _om A ~~ x )
2 bren 
 |-  ( A ~~ x <-> E. f f : A -1-1-onto-> x )
3 pssss 
 |-  ( B C. A -> B C_ A )
4 imass2 
 |-  ( B C_ A -> ( f " B ) C_ ( f " A ) )
5 3 4 syl 
 |-  ( B C. A -> ( f " B ) C_ ( f " A ) )
6 5 adantl 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C_ ( f " A ) )
7 pssnel 
 |-  ( B C. A -> E. y ( y e. A /\ -. y e. B ) )
8 eldif 
 |-  ( y e. ( A \ B ) <-> ( y e. A /\ -. y e. B ) )
9 f1ofn 
 |-  ( f : A -1-1-onto-> x -> f Fn A )
10 difss 
 |-  ( A \ B ) C_ A
11 fnfvima 
 |-  ( ( f Fn A /\ ( A \ B ) C_ A /\ y e. ( A \ B ) ) -> ( f ` y ) e. ( f " ( A \ B ) ) )
12 11 3expia 
 |-  ( ( f Fn A /\ ( A \ B ) C_ A ) -> ( y e. ( A \ B ) -> ( f ` y ) e. ( f " ( A \ B ) ) ) )
13 9 10 12 sylancl 
 |-  ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> ( f ` y ) e. ( f " ( A \ B ) ) ) )
14 dff1o3 
 |-  ( f : A -1-1-onto-> x <-> ( f : A -onto-> x /\ Fun `' f ) )
15 imadif 
 |-  ( Fun `' f -> ( f " ( A \ B ) ) = ( ( f " A ) \ ( f " B ) ) )
16 14 15 simplbiim 
 |-  ( f : A -1-1-onto-> x -> ( f " ( A \ B ) ) = ( ( f " A ) \ ( f " B ) ) )
17 16 eleq2d 
 |-  ( f : A -1-1-onto-> x -> ( ( f ` y ) e. ( f " ( A \ B ) ) <-> ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) ) )
18 13 17 sylibd 
 |-  ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) ) )
19 n0i 
 |-  ( ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
20 18 19 syl6 
 |-  ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
21 8 20 syl5bir 
 |-  ( f : A -1-1-onto-> x -> ( ( y e. A /\ -. y e. B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
22 21 exlimdv 
 |-  ( f : A -1-1-onto-> x -> ( E. y ( y e. A /\ -. y e. B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
23 22 imp 
 |-  ( ( f : A -1-1-onto-> x /\ E. y ( y e. A /\ -. y e. B ) ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
24 7 23 sylan2 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
25 ssdif0 
 |-  ( ( f " A ) C_ ( f " B ) <-> ( ( f " A ) \ ( f " B ) ) = (/) )
26 24 25 sylnibr 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> -. ( f " A ) C_ ( f " B ) )
27 dfpss3 
 |-  ( ( f " B ) C. ( f " A ) <-> ( ( f " B ) C_ ( f " A ) /\ -. ( f " A ) C_ ( f " B ) ) )
28 6 26 27 sylanbrc 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C. ( f " A ) )
29 imadmrn 
 |-  ( f " dom f ) = ran f
30 f1odm 
 |-  ( f : A -1-1-onto-> x -> dom f = A )
31 30 imaeq2d 
 |-  ( f : A -1-1-onto-> x -> ( f " dom f ) = ( f " A ) )
32 f1ofo 
 |-  ( f : A -1-1-onto-> x -> f : A -onto-> x )
33 forn 
 |-  ( f : A -onto-> x -> ran f = x )
34 32 33 syl 
 |-  ( f : A -1-1-onto-> x -> ran f = x )
35 29 31 34 3eqtr3a 
 |-  ( f : A -1-1-onto-> x -> ( f " A ) = x )
36 35 psseq2d 
 |-  ( f : A -1-1-onto-> x -> ( ( f " B ) C. ( f " A ) <-> ( f " B ) C. x ) )
37 36 adantr 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( ( f " B ) C. ( f " A ) <-> ( f " B ) C. x ) )
38 28 37 mpbid 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C. x )
39 php2 
 |-  ( ( x e. _om /\ ( f " B ) C. x ) -> ( f " B ) ~< x )
40 38 39 sylan2 
 |-  ( ( x e. _om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> ( f " B ) ~< x )
41 nnfi 
 |-  ( x e. _om -> x e. Fin )
42 f1of1 
 |-  ( f : A -1-1-onto-> x -> f : A -1-1-> x )
43 f1ores 
 |-  ( ( f : A -1-1-> x /\ B C_ A ) -> ( f |` B ) : B -1-1-onto-> ( f " B ) )
44 42 3 43 syl2an 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f |` B ) : B -1-1-onto-> ( f " B ) )
45 vex 
 |-  f e. _V
46 45 resex 
 |-  ( f |` B ) e. _V
47 f1oeq1 
 |-  ( y = ( f |` B ) -> ( y : B -1-1-onto-> ( f " B ) <-> ( f |` B ) : B -1-1-onto-> ( f " B ) ) )
48 46 47 spcev 
 |-  ( ( f |` B ) : B -1-1-onto-> ( f " B ) -> E. y y : B -1-1-onto-> ( f " B ) )
49 bren 
 |-  ( B ~~ ( f " B ) <-> E. y y : B -1-1-onto-> ( f " B ) )
50 48 49 sylibr 
 |-  ( ( f |` B ) : B -1-1-onto-> ( f " B ) -> B ~~ ( f " B ) )
51 44 50 syl 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> B ~~ ( f " B ) )
52 endom 
 |-  ( B ~~ ( f " B ) -> B ~<_ ( f " B ) )
53 sdomdom 
 |-  ( ( f " B ) ~< x -> ( f " B ) ~<_ x )
54 domfi 
 |-  ( ( x e. Fin /\ ( f " B ) ~<_ x ) -> ( f " B ) e. Fin )
55 53 54 sylan2 
 |-  ( ( x e. Fin /\ ( f " B ) ~< x ) -> ( f " B ) e. Fin )
56 55 3adant2 
 |-  ( ( x e. Fin /\ B ~<_ ( f " B ) /\ ( f " B ) ~< x ) -> ( f " B ) e. Fin )
57 domfi 
 |-  ( ( ( f " B ) e. Fin /\ B ~<_ ( f " B ) ) -> B e. Fin )
58 57 3adant3 
 |-  ( ( ( f " B ) e. Fin /\ B ~<_ ( f " B ) /\ ( f " B ) ~< x ) -> B e. Fin )
59 domsdomtrfi 
 |-  ( ( B e. Fin /\ B ~<_ ( f " B ) /\ ( f " B ) ~< x ) -> B ~< x )
60 58 59 syld3an1 
 |-  ( ( ( f " B ) e. Fin /\ B ~<_ ( f " B ) /\ ( f " B ) ~< x ) -> B ~< x )
61 56 60 syld3an1 
 |-  ( ( x e. Fin /\ B ~<_ ( f " B ) /\ ( f " B ) ~< x ) -> B ~< x )
62 52 61 syl3an2 
 |-  ( ( x e. Fin /\ B ~~ ( f " B ) /\ ( f " B ) ~< x ) -> B ~< x )
63 62 3expia 
 |-  ( ( x e. Fin /\ B ~~ ( f " B ) ) -> ( ( f " B ) ~< x -> B ~< x ) )
64 41 51 63 syl2an 
 |-  ( ( x e. _om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> ( ( f " B ) ~< x -> B ~< x ) )
65 40 64 mpd 
 |-  ( ( x e. _om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> B ~< x )
66 65 exp32 
 |-  ( x e. _om -> ( f : A -1-1-onto-> x -> ( B C. A -> B ~< x ) ) )
67 66 exlimdv 
 |-  ( x e. _om -> ( E. f f : A -1-1-onto-> x -> ( B C. A -> B ~< x ) ) )
68 2 67 syl5bi 
 |-  ( x e. _om -> ( A ~~ x -> ( B C. A -> B ~< x ) ) )
69 ensymfib 
 |-  ( x e. Fin -> ( x ~~ A <-> A ~~ x ) )
70 69 adantr 
 |-  ( ( x e. Fin /\ B ~< x ) -> ( x ~~ A <-> A ~~ x ) )
71 70 biimp3ar 
 |-  ( ( x e. Fin /\ B ~< x /\ A ~~ x ) -> x ~~ A )
72 endom 
 |-  ( x ~~ A -> x ~<_ A )
73 sdomdom 
 |-  ( B ~< x -> B ~<_ x )
74 domfi 
 |-  ( ( x e. Fin /\ B ~<_ x ) -> B e. Fin )
75 73 74 sylan2 
 |-  ( ( x e. Fin /\ B ~< x ) -> B e. Fin )
76 75 3adant3 
 |-  ( ( x e. Fin /\ B ~< x /\ x ~<_ A ) -> B e. Fin )
77 sdomdomtrfi 
 |-  ( ( B e. Fin /\ B ~< x /\ x ~<_ A ) -> B ~< A )
78 76 77 syld3an1 
 |-  ( ( x e. Fin /\ B ~< x /\ x ~<_ A ) -> B ~< A )
79 72 78 syl3an3 
 |-  ( ( x e. Fin /\ B ~< x /\ x ~~ A ) -> B ~< A )
80 71 79 syld3an3 
 |-  ( ( x e. Fin /\ B ~< x /\ A ~~ x ) -> B ~< A )
81 41 80 syl3an1 
 |-  ( ( x e. _om /\ B ~< x /\ A ~~ x ) -> B ~< A )
82 81 3com23 
 |-  ( ( x e. _om /\ A ~~ x /\ B ~< x ) -> B ~< A )
83 82 3exp 
 |-  ( x e. _om -> ( A ~~ x -> ( B ~< x -> B ~< A ) ) )
84 68 83 syldd 
 |-  ( x e. _om -> ( A ~~ x -> ( B C. A -> B ~< A ) ) )
85 84 rexlimiv 
 |-  ( E. x e. _om A ~~ x -> ( B C. A -> B ~< A ) )
86 1 85 sylbi 
 |-  ( A e. Fin -> ( B C. A -> B ~< A ) )
87 86 imp 
 |-  ( ( A e. Fin /\ B C. A ) -> B ~< A )