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)

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 relen 
 |-  Rel ~~
3 2 brrelex1i 
 |-  ( A ~~ x -> A e. _V )
4 pssss 
 |-  ( B C. A -> B C_ A )
5 ssdomg 
 |-  ( A e. _V -> ( B C_ A -> B ~<_ A ) )
6 5 imp 
 |-  ( ( A e. _V /\ B C_ A ) -> B ~<_ A )
7 3 4 6 syl2an 
 |-  ( ( A ~~ x /\ B C. A ) -> B ~<_ A )
8 7 adantll 
 |-  ( ( ( x e. _om /\ A ~~ x ) /\ B C. A ) -> B ~<_ A )
9 bren 
 |-  ( A ~~ x <-> E. f f : A -1-1-onto-> x )
10 imass2 
 |-  ( B C_ A -> ( f " B ) C_ ( f " A ) )
11 4 10 syl 
 |-  ( B C. A -> ( f " B ) C_ ( f " A ) )
12 11 adantl 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C_ ( f " A ) )
13 pssnel 
 |-  ( B C. A -> E. y ( y e. A /\ -. y e. B ) )
14 eldif 
 |-  ( y e. ( A \ B ) <-> ( y e. A /\ -. y e. B ) )
15 f1ofn 
 |-  ( f : A -1-1-onto-> x -> f Fn A )
16 difss 
 |-  ( A \ B ) C_ A
17 fnfvima 
 |-  ( ( f Fn A /\ ( A \ B ) C_ A /\ y e. ( A \ B ) ) -> ( f ` y ) e. ( f " ( A \ B ) ) )
18 17 3expia 
 |-  ( ( f Fn A /\ ( A \ B ) C_ A ) -> ( y e. ( A \ B ) -> ( f ` y ) e. ( f " ( A \ B ) ) ) )
19 15 16 18 sylancl 
 |-  ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> ( f ` y ) e. ( f " ( A \ B ) ) ) )
20 dff1o3 
 |-  ( f : A -1-1-onto-> x <-> ( f : A -onto-> x /\ Fun `' f ) )
21 imadif 
 |-  ( Fun `' f -> ( f " ( A \ B ) ) = ( ( f " A ) \ ( f " B ) ) )
22 20 21 simplbiim 
 |-  ( f : A -1-1-onto-> x -> ( f " ( A \ B ) ) = ( ( f " A ) \ ( f " B ) ) )
23 22 eleq2d 
 |-  ( f : A -1-1-onto-> x -> ( ( f ` y ) e. ( f " ( A \ B ) ) <-> ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) ) )
24 19 23 sylibd 
 |-  ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) ) )
25 n0i 
 |-  ( ( f ` y ) e. ( ( f " A ) \ ( f " B ) ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
26 24 25 syl6 
 |-  ( f : A -1-1-onto-> x -> ( y e. ( A \ B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
27 14 26 syl5bir 
 |-  ( f : A -1-1-onto-> x -> ( ( y e. A /\ -. y e. B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
28 27 exlimdv 
 |-  ( f : A -1-1-onto-> x -> ( E. y ( y e. A /\ -. y e. B ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) ) )
29 28 imp 
 |-  ( ( f : A -1-1-onto-> x /\ E. y ( y e. A /\ -. y e. B ) ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
30 13 29 sylan2 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> -. ( ( f " A ) \ ( f " B ) ) = (/) )
31 ssdif0 
 |-  ( ( f " A ) C_ ( f " B ) <-> ( ( f " A ) \ ( f " B ) ) = (/) )
32 30 31 sylnibr 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> -. ( f " A ) C_ ( f " B ) )
33 dfpss3 
 |-  ( ( f " B ) C. ( f " A ) <-> ( ( f " B ) C_ ( f " A ) /\ -. ( f " A ) C_ ( f " B ) ) )
34 12 32 33 sylanbrc 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C. ( f " A ) )
35 imadmrn 
 |-  ( f " dom f ) = ran f
36 f1odm 
 |-  ( f : A -1-1-onto-> x -> dom f = A )
37 36 imaeq2d 
 |-  ( f : A -1-1-onto-> x -> ( f " dom f ) = ( f " A ) )
38 f1ofo 
 |-  ( f : A -1-1-onto-> x -> f : A -onto-> x )
39 forn 
 |-  ( f : A -onto-> x -> ran f = x )
40 38 39 syl 
 |-  ( f : A -1-1-onto-> x -> ran f = x )
41 35 37 40 3eqtr3a 
 |-  ( f : A -1-1-onto-> x -> ( f " A ) = x )
42 41 psseq2d 
 |-  ( f : A -1-1-onto-> x -> ( ( f " B ) C. ( f " A ) <-> ( f " B ) C. x ) )
43 42 adantr 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( ( f " B ) C. ( f " A ) <-> ( f " B ) C. x ) )
44 34 43 mpbid 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f " B ) C. x )
45 php 
 |-  ( ( x e. _om /\ ( f " B ) C. x ) -> -. x ~~ ( f " B ) )
46 44 45 sylan2 
 |-  ( ( x e. _om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> -. x ~~ ( f " B ) )
47 f1of1 
 |-  ( f : A -1-1-onto-> x -> f : A -1-1-> x )
48 f1ores 
 |-  ( ( f : A -1-1-> x /\ B C_ A ) -> ( f |` B ) : B -1-1-onto-> ( f " B ) )
49 47 4 48 syl2an 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( f |` B ) : B -1-1-onto-> ( f " B ) )
50 vex 
 |-  f e. _V
51 50 resex 
 |-  ( f |` B ) e. _V
52 f1oeq1 
 |-  ( y = ( f |` B ) -> ( y : B -1-1-onto-> ( f " B ) <-> ( f |` B ) : B -1-1-onto-> ( f " B ) ) )
53 51 52 spcev 
 |-  ( ( f |` B ) : B -1-1-onto-> ( f " B ) -> E. y y : B -1-1-onto-> ( f " B ) )
54 bren 
 |-  ( B ~~ ( f " B ) <-> E. y y : B -1-1-onto-> ( f " B ) )
55 53 54 sylibr 
 |-  ( ( f |` B ) : B -1-1-onto-> ( f " B ) -> B ~~ ( f " B ) )
56 49 55 syl 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> B ~~ ( f " B ) )
57 entr 
 |-  ( ( x ~~ B /\ B ~~ ( f " B ) ) -> x ~~ ( f " B ) )
58 57 expcom 
 |-  ( B ~~ ( f " B ) -> ( x ~~ B -> x ~~ ( f " B ) ) )
59 56 58 syl 
 |-  ( ( f : A -1-1-onto-> x /\ B C. A ) -> ( x ~~ B -> x ~~ ( f " B ) ) )
60 59 adantl 
 |-  ( ( x e. _om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> ( x ~~ B -> x ~~ ( f " B ) ) )
61 46 60 mtod 
 |-  ( ( x e. _om /\ ( f : A -1-1-onto-> x /\ B C. A ) ) -> -. x ~~ B )
62 61 exp32 
 |-  ( x e. _om -> ( f : A -1-1-onto-> x -> ( B C. A -> -. x ~~ B ) ) )
63 62 exlimdv 
 |-  ( x e. _om -> ( E. f f : A -1-1-onto-> x -> ( B C. A -> -. x ~~ B ) ) )
64 9 63 syl5bi 
 |-  ( x e. _om -> ( A ~~ x -> ( B C. A -> -. x ~~ B ) ) )
65 64 imp31 
 |-  ( ( ( x e. _om /\ A ~~ x ) /\ B C. A ) -> -. x ~~ B )
66 entr 
 |-  ( ( B ~~ A /\ A ~~ x ) -> B ~~ x )
67 66 ex 
 |-  ( B ~~ A -> ( A ~~ x -> B ~~ x ) )
68 ensym 
 |-  ( B ~~ x -> x ~~ B )
69 67 68 syl6com 
 |-  ( A ~~ x -> ( B ~~ A -> x ~~ B ) )
70 69 ad2antlr 
 |-  ( ( ( x e. _om /\ A ~~ x ) /\ B C. A ) -> ( B ~~ A -> x ~~ B ) )
71 65 70 mtod 
 |-  ( ( ( x e. _om /\ A ~~ x ) /\ B C. A ) -> -. B ~~ A )
72 brsdom 
 |-  ( B ~< A <-> ( B ~<_ A /\ -. B ~~ A ) )
73 8 71 72 sylanbrc 
 |-  ( ( ( x e. _om /\ A ~~ x ) /\ B C. A ) -> B ~< A )
74 73 exp31 
 |-  ( x e. _om -> ( A ~~ x -> ( B C. A -> B ~< A ) ) )
75 74 rexlimiv 
 |-  ( E. x e. _om A ~~ x -> ( B C. A -> B ~< A ) )
76 1 75 sylbi 
 |-  ( A e. Fin -> ( B C. A -> B ~< A ) )
77 76 imp 
 |-  ( ( A e. Fin /\ B C. A ) -> B ~< A )