Metamath Proof Explorer

Theorem php

Description: Pigeonhole Principle. A natural number is not equinumerous to a proper subset of itself. Theorem (Pigeonhole Principle) of Enderton p. 134. The theorem is so-called because you can't putn + 1 pigeons inton holes (if each hole holds only one pigeon). The proof consists of lemmas phplem1 through phplem4 , nneneq , and this final piece of the proof. (Contributed by NM, 29-May-1998)

Ref Expression
Assertion php 
|- ( ( A e. _om /\ B C. A ) -> -. A ~~ B )

Proof

Step Hyp Ref Expression
1 0ss 
 |-  (/) C_ B
2 sspsstr 
 |-  ( ( (/) C_ B /\ B C. A ) -> (/) C. A )
3 1 2 mpan 
 |-  ( B C. A -> (/) C. A )
4 0pss 
 |-  ( (/) C. A <-> A =/= (/) )
5 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
6 4 5 bitri 
 |-  ( (/) C. A <-> -. A = (/) )
7 3 6 sylib 
 |-  ( B C. A -> -. A = (/) )
8 nn0suc 
 |-  ( A e. _om -> ( A = (/) \/ E. x e. _om A = suc x ) )
9 8 orcanai 
 |-  ( ( A e. _om /\ -. A = (/) ) -> E. x e. _om A = suc x )
10 7 9 sylan2 
 |-  ( ( A e. _om /\ B C. A ) -> E. x e. _om A = suc x )
11 pssnel 
 |-  ( B C. suc x -> E. y ( y e. suc x /\ -. y e. B ) )
12 pssss 
 |-  ( B C. suc x -> B C_ suc x )
13 ssdif 
 |-  ( B C_ suc x -> ( B \ { y } ) C_ ( suc x \ { y } ) )
14 disjsn 
 |-  ( ( B i^i { y } ) = (/) <-> -. y e. B )
15 disj3 
 |-  ( ( B i^i { y } ) = (/) <-> B = ( B \ { y } ) )
16 14 15 bitr3i 
 |-  ( -. y e. B <-> B = ( B \ { y } ) )
17 sseq1 
 |-  ( B = ( B \ { y } ) -> ( B C_ ( suc x \ { y } ) <-> ( B \ { y } ) C_ ( suc x \ { y } ) ) )
18 16 17 sylbi 
 |-  ( -. y e. B -> ( B C_ ( suc x \ { y } ) <-> ( B \ { y } ) C_ ( suc x \ { y } ) ) )
19 13 18 syl5ibr 
 |-  ( -. y e. B -> ( B C_ suc x -> B C_ ( suc x \ { y } ) ) )
20 vex 
 |-  x e. _V
21 20 sucex 
 |-  suc x e. _V
22 21 difexi 
 |-  ( suc x \ { y } ) e. _V
23 ssdomg 
 |-  ( ( suc x \ { y } ) e. _V -> ( B C_ ( suc x \ { y } ) -> B ~<_ ( suc x \ { y } ) ) )
24 22 23 ax-mp 
 |-  ( B C_ ( suc x \ { y } ) -> B ~<_ ( suc x \ { y } ) )
25 12 19 24 syl56 
 |-  ( -. y e. B -> ( B C. suc x -> B ~<_ ( suc x \ { y } ) ) )
26 25 imp 
 |-  ( ( -. y e. B /\ B C. suc x ) -> B ~<_ ( suc x \ { y } ) )
27 vex 
 |-  y e. _V
28 20 27 phplem3 
 |-  ( ( x e. _om /\ y e. suc x ) -> x ~~ ( suc x \ { y } ) )
29 28 ensymd 
 |-  ( ( x e. _om /\ y e. suc x ) -> ( suc x \ { y } ) ~~ x )
30 domentr 
 |-  ( ( B ~<_ ( suc x \ { y } ) /\ ( suc x \ { y } ) ~~ x ) -> B ~<_ x )
31 26 29 30 syl2an 
 |-  ( ( ( -. y e. B /\ B C. suc x ) /\ ( x e. _om /\ y e. suc x ) ) -> B ~<_ x )
32 31 exp43 
 |-  ( -. y e. B -> ( B C. suc x -> ( x e. _om -> ( y e. suc x -> B ~<_ x ) ) ) )
33 32 com4r 
 |-  ( y e. suc x -> ( -. y e. B -> ( B C. suc x -> ( x e. _om -> B ~<_ x ) ) ) )
34 33 imp 
 |-  ( ( y e. suc x /\ -. y e. B ) -> ( B C. suc x -> ( x e. _om -> B ~<_ x ) ) )
35 34 exlimiv 
 |-  ( E. y ( y e. suc x /\ -. y e. B ) -> ( B C. suc x -> ( x e. _om -> B ~<_ x ) ) )
36 11 35 mpcom 
 |-  ( B C. suc x -> ( x e. _om -> B ~<_ x ) )
37 endomtr 
 |-  ( ( suc x ~~ B /\ B ~<_ x ) -> suc x ~<_ x )
38 sssucid 
 |-  x C_ suc x
39 ssdomg 
 |-  ( suc x e. _V -> ( x C_ suc x -> x ~<_ suc x ) )
40 21 38 39 mp2 
 |-  x ~<_ suc x
41 sbth 
 |-  ( ( suc x ~<_ x /\ x ~<_ suc x ) -> suc x ~~ x )
42 37 40 41 sylancl 
 |-  ( ( suc x ~~ B /\ B ~<_ x ) -> suc x ~~ x )
43 42 expcom 
 |-  ( B ~<_ x -> ( suc x ~~ B -> suc x ~~ x ) )
44 peano2b 
 |-  ( x e. _om <-> suc x e. _om )
45 nnord 
 |-  ( suc x e. _om -> Ord suc x )
46 44 45 sylbi 
 |-  ( x e. _om -> Ord suc x )
47 20 sucid 
 |-  x e. suc x
48 nordeq 
 |-  ( ( Ord suc x /\ x e. suc x ) -> suc x =/= x )
49 46 47 48 sylancl 
 |-  ( x e. _om -> suc x =/= x )
50 nneneq 
 |-  ( ( suc x e. _om /\ x e. _om ) -> ( suc x ~~ x <-> suc x = x ) )
51 44 50 sylanb 
 |-  ( ( x e. _om /\ x e. _om ) -> ( suc x ~~ x <-> suc x = x ) )
52 51 anidms 
 |-  ( x e. _om -> ( suc x ~~ x <-> suc x = x ) )
53 52 necon3bbid 
 |-  ( x e. _om -> ( -. suc x ~~ x <-> suc x =/= x ) )
54 49 53 mpbird 
 |-  ( x e. _om -> -. suc x ~~ x )
55 43 54 nsyli 
 |-  ( B ~<_ x -> ( x e. _om -> -. suc x ~~ B ) )
56 36 55 syli 
 |-  ( B C. suc x -> ( x e. _om -> -. suc x ~~ B ) )
57 56 com12 
 |-  ( x e. _om -> ( B C. suc x -> -. suc x ~~ B ) )
58 psseq2 
 |-  ( A = suc x -> ( B C. A <-> B C. suc x ) )
59 breq1 
 |-  ( A = suc x -> ( A ~~ B <-> suc x ~~ B ) )
60 59 notbid 
 |-  ( A = suc x -> ( -. A ~~ B <-> -. suc x ~~ B ) )
61 58 60 imbi12d 
 |-  ( A = suc x -> ( ( B C. A -> -. A ~~ B ) <-> ( B C. suc x -> -. suc x ~~ B ) ) )
62 57 61 syl5ibrcom 
 |-  ( x e. _om -> ( A = suc x -> ( B C. A -> -. A ~~ B ) ) )
63 62 rexlimiv 
 |-  ( E. x e. _om A = suc x -> ( B C. A -> -. A ~~ B ) )
64 10 63 syl 
 |-  ( ( A e. _om /\ B C. A ) -> ( B C. A -> -. A ~~ B ) )
65 64 ex 
 |-  ( A e. _om -> ( B C. A -> ( B C. A -> -. A ~~ B ) ) )
66 65 pm2.43d 
 |-  ( A e. _om -> ( B C. A -> -. A ~~ B ) )
67 66 imp 
 |-  ( ( A e. _om /\ B C. A ) -> -. A ~~ B )