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 phplem1 , phplem2 , nneneq , and this final piece of the proof. (Contributed by NM, 29-May-1998) Avoid ax-pow . (Revised by BTernaryTau, 18-Nov-2024)

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 imbitrrid
 |-  ( -. y e. B -> ( B C_ suc x -> B C_ ( suc x \ { y } ) ) )
20 12 19 syl5
 |-  ( -. y e. B -> ( B C. suc x -> B C_ ( suc x \ { y } ) ) )
21 peano2
 |-  ( x e. _om -> suc x e. _om )
22 nnfi
 |-  ( suc x e. _om -> suc x e. Fin )
23 diffi
 |-  ( suc x e. Fin -> ( suc x \ { y } ) e. Fin )
24 ssdomfi
 |-  ( ( suc x \ { y } ) e. Fin -> ( B C_ ( suc x \ { y } ) -> B ~<_ ( suc x \ { y } ) ) )
25 21 22 23 24 4syl
 |-  ( x e. _om -> ( B C_ ( suc x \ { y } ) -> B ~<_ ( suc x \ { y } ) ) )
26 20 25 sylan9
 |-  ( ( -. y e. B /\ x e. _om ) -> ( B C. suc x -> B ~<_ ( suc x \ { y } ) ) )
27 26 3impia
 |-  ( ( -. y e. B /\ x e. _om /\ B C. suc x ) -> B ~<_ ( suc x \ { y } ) )
28 27 3com23
 |-  ( ( -. y e. B /\ B C. suc x /\ x e. _om ) -> B ~<_ ( suc x \ { y } ) )
29 28 3expa
 |-  ( ( ( -. y e. B /\ B C. suc x ) /\ x e. _om ) -> B ~<_ ( suc x \ { y } ) )
30 29 adantrr
 |-  ( ( ( -. y e. B /\ B C. suc x ) /\ ( x e. _om /\ y e. suc x ) ) -> B ~<_ ( suc x \ { y } ) )
31 nnfi
 |-  ( x e. _om -> x e. Fin )
32 31 ad2antrl
 |-  ( ( B ~<_ ( suc x \ { y } ) /\ ( x e. _om /\ y e. suc x ) ) -> x e. Fin )
33 simpl
 |-  ( ( B ~<_ ( suc x \ { y } ) /\ ( x e. _om /\ y e. suc x ) ) -> B ~<_ ( suc x \ { y } ) )
34 simpr
 |-  ( ( B ~<_ ( suc x \ { y } ) /\ ( x e. _om /\ y e. suc x ) ) -> ( x e. _om /\ y e. suc x ) )
35 phplem1
 |-  ( ( x e. _om /\ y e. suc x ) -> x ~~ ( suc x \ { y } ) )
36 ensymfib
 |-  ( x e. Fin -> ( x ~~ ( suc x \ { y } ) <-> ( suc x \ { y } ) ~~ x ) )
37 31 36 syl
 |-  ( x e. _om -> ( x ~~ ( suc x \ { y } ) <-> ( suc x \ { y } ) ~~ x ) )
38 37 adantr
 |-  ( ( x e. _om /\ y e. suc x ) -> ( x ~~ ( suc x \ { y } ) <-> ( suc x \ { y } ) ~~ x ) )
39 35 38 mpbid
 |-  ( ( x e. _om /\ y e. suc x ) -> ( suc x \ { y } ) ~~ x )
40 endom
 |-  ( ( suc x \ { y } ) ~~ x -> ( suc x \ { y } ) ~<_ x )
41 39 40 syl
 |-  ( ( x e. _om /\ y e. suc x ) -> ( suc x \ { y } ) ~<_ x )
42 domtrfir
 |-  ( ( x e. Fin /\ B ~<_ ( suc x \ { y } ) /\ ( suc x \ { y } ) ~<_ x ) -> B ~<_ x )
43 41 42 syl3an3
 |-  ( ( x e. Fin /\ B ~<_ ( suc x \ { y } ) /\ ( x e. _om /\ y e. suc x ) ) -> B ~<_ x )
44 32 33 34 43 syl3anc
 |-  ( ( B ~<_ ( suc x \ { y } ) /\ ( x e. _om /\ y e. suc x ) ) -> B ~<_ x )
45 30 44 sylancom
 |-  ( ( ( -. y e. B /\ B C. suc x ) /\ ( x e. _om /\ y e. suc x ) ) -> B ~<_ x )
46 45 exp43
 |-  ( -. y e. B -> ( B C. suc x -> ( x e. _om -> ( y e. suc x -> B ~<_ x ) ) ) )
47 46 com4r
 |-  ( y e. suc x -> ( -. y e. B -> ( B C. suc x -> ( x e. _om -> B ~<_ x ) ) ) )
48 47 imp
 |-  ( ( y e. suc x /\ -. y e. B ) -> ( B C. suc x -> ( x e. _om -> B ~<_ x ) ) )
49 48 exlimiv
 |-  ( E. y ( y e. suc x /\ -. y e. B ) -> ( B C. suc x -> ( x e. _om -> B ~<_ x ) ) )
50 11 49 mpcom
 |-  ( B C. suc x -> ( x e. _om -> B ~<_ x ) )
51 simp1
 |-  ( ( x e. _om /\ suc x ~~ B /\ B ~<_ x ) -> x e. _om )
52 endom
 |-  ( suc x ~~ B -> suc x ~<_ B )
53 domtrfir
 |-  ( ( x e. Fin /\ suc x ~<_ B /\ B ~<_ x ) -> suc x ~<_ x )
54 52 53 syl3an2
 |-  ( ( x e. Fin /\ suc x ~~ B /\ B ~<_ x ) -> suc x ~<_ x )
55 31 54 syl3an1
 |-  ( ( x e. _om /\ suc x ~~ B /\ B ~<_ x ) -> suc x ~<_ x )
56 sssucid
 |-  x C_ suc x
57 ssdomfi
 |-  ( suc x e. Fin -> ( x C_ suc x -> x ~<_ suc x ) )
58 22 56 57 mpisyl
 |-  ( suc x e. _om -> x ~<_ suc x )
59 21 58 syl
 |-  ( x e. _om -> x ~<_ suc x )
60 59 adantr
 |-  ( ( x e. _om /\ suc x ~<_ x ) -> x ~<_ suc x )
61 sbthfi
 |-  ( ( x e. Fin /\ suc x ~<_ x /\ x ~<_ suc x ) -> suc x ~~ x )
62 31 61 syl3an1
 |-  ( ( x e. _om /\ suc x ~<_ x /\ x ~<_ suc x ) -> suc x ~~ x )
63 60 62 mpd3an3
 |-  ( ( x e. _om /\ suc x ~<_ x ) -> suc x ~~ x )
64 51 55 63 syl2anc
 |-  ( ( x e. _om /\ suc x ~~ B /\ B ~<_ x ) -> suc x ~~ x )
65 64 3com23
 |-  ( ( x e. _om /\ B ~<_ x /\ suc x ~~ B ) -> suc x ~~ x )
66 65 3expia
 |-  ( ( x e. _om /\ B ~<_ x ) -> ( suc x ~~ B -> suc x ~~ x ) )
67 peano2b
 |-  ( x e. _om <-> suc x e. _om )
68 nnord
 |-  ( suc x e. _om -> Ord suc x )
69 67 68 sylbi
 |-  ( x e. _om -> Ord suc x )
70 vex
 |-  x e. _V
71 70 sucid
 |-  x e. suc x
72 nordeq
 |-  ( ( Ord suc x /\ x e. suc x ) -> suc x =/= x )
73 69 71 72 sylancl
 |-  ( x e. _om -> suc x =/= x )
74 nneneq
 |-  ( ( suc x e. _om /\ x e. _om ) -> ( suc x ~~ x <-> suc x = x ) )
75 67 74 sylanb
 |-  ( ( x e. _om /\ x e. _om ) -> ( suc x ~~ x <-> suc x = x ) )
76 75 anidms
 |-  ( x e. _om -> ( suc x ~~ x <-> suc x = x ) )
77 76 necon3bbid
 |-  ( x e. _om -> ( -. suc x ~~ x <-> suc x =/= x ) )
78 73 77 mpbird
 |-  ( x e. _om -> -. suc x ~~ x )
79 66 78 nsyli
 |-  ( ( x e. _om /\ B ~<_ x ) -> ( x e. _om -> -. suc x ~~ B ) )
80 79 expcom
 |-  ( B ~<_ x -> ( x e. _om -> ( x e. _om -> -. suc x ~~ B ) ) )
81 80 pm2.43d
 |-  ( B ~<_ x -> ( x e. _om -> -. suc x ~~ B ) )
82 50 81 syli
 |-  ( B C. suc x -> ( x e. _om -> -. suc x ~~ B ) )
83 82 com12
 |-  ( x e. _om -> ( B C. suc x -> -. suc x ~~ B ) )
84 psseq2
 |-  ( A = suc x -> ( B C. A <-> B C. suc x ) )
85 breq1
 |-  ( A = suc x -> ( A ~~ B <-> suc x ~~ B ) )
86 85 notbid
 |-  ( A = suc x -> ( -. A ~~ B <-> -. suc x ~~ B ) )
87 84 86 imbi12d
 |-  ( A = suc x -> ( ( B C. A -> -. A ~~ B ) <-> ( B C. suc x -> -. suc x ~~ B ) ) )
88 83 87 syl5ibrcom
 |-  ( x e. _om -> ( A = suc x -> ( B C. A -> -. A ~~ B ) ) )
89 88 rexlimiv
 |-  ( E. x e. _om A = suc x -> ( B C. A -> -. A ~~ B ) )
90 10 89 syl
 |-  ( ( A e. _om /\ B C. A ) -> ( B C. A -> -. A ~~ B ) )
91 90 syldbl2
 |-  ( ( A e. _om /\ B C. A ) -> -. A ~~ B )