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 ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ¬ 𝐴 ≈ 𝐵 )

Proof

Step Hyp Ref Expression
1 0ss ⊢ ∅ ⊆ 𝐵
2 sspsstr ⊢ ( ( ∅ ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐴 ) → ∅ ⊊ 𝐴 )
3 1 2 mpan ⊢ ( 𝐵 ⊊ 𝐴 → ∅ ⊊ 𝐴 )
4 0pss ⊢ ( ∅ ⊊ 𝐴 ↔ 𝐴 ≠ ∅ )
5 df-ne ⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
6 4 5 bitri ⊢ ( ∅ ⊊ 𝐴 ↔ ¬ 𝐴 = ∅ )
7 3 6 sylib ⊢ ( 𝐵 ⊊ 𝐴 → ¬ 𝐴 = ∅ )
8 nn0suc ⊢ ( 𝐴 ∈ ω → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 ) )
9 8 orcanai ⊢ ( ( 𝐴 ∈ ω ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 )
10 7 9 sylan2 ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 )
11 pssnel ⊢ ( 𝐵 ⊊ suc 𝑥 → ∃ 𝑦 ( 𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵 ) )
12 pssss ⊢ ( 𝐵 ⊊ suc 𝑥 → 𝐵 ⊆ suc 𝑥 )
13 ssdif ⊢ ( 𝐵 ⊆ suc 𝑥 → ( 𝐵 ∖ { 𝑦 } ) ⊆ ( suc 𝑥 ∖ { 𝑦 } ) )
14 disjsn ⊢ ( ( 𝐵 ∩ { 𝑦 } ) = ∅ ↔ ¬ 𝑦 ∈ 𝐵 )
15 disj3 ⊢ ( ( 𝐵 ∩ { 𝑦 } ) = ∅ ↔ 𝐵 = ( 𝐵 ∖ { 𝑦 } ) )
16 14 15 bitr3i ⊢ ( ¬ 𝑦 ∈ 𝐵 ↔ 𝐵 = ( 𝐵 ∖ { 𝑦 } ) )
17 sseq1 ⊢ ( 𝐵 = ( 𝐵 ∖ { 𝑦 } ) → ( 𝐵 ⊆ ( suc 𝑥 ∖ { 𝑦 } ) ↔ ( 𝐵 ∖ { 𝑦 } ) ⊆ ( suc 𝑥 ∖ { 𝑦 } ) ) )
18 16 17 sylbi ⊢ ( ¬ 𝑦 ∈ 𝐵 → ( 𝐵 ⊆ ( suc 𝑥 ∖ { 𝑦 } ) ↔ ( 𝐵 ∖ { 𝑦 } ) ⊆ ( suc 𝑥 ∖ { 𝑦 } ) ) )
19 13 18 syl5ibr ⊢ ( ¬ 𝑦 ∈ 𝐵 → ( 𝐵 ⊆ suc 𝑥 → 𝐵 ⊆ ( suc 𝑥 ∖ { 𝑦 } ) ) )
20 12 19 syl5 ⊢ ( ¬ 𝑦 ∈ 𝐵 → ( 𝐵 ⊊ suc 𝑥 → 𝐵 ⊆ ( suc 𝑥 ∖ { 𝑦 } ) ) )
21 peano2 ⊢ ( 𝑥 ∈ ω → suc 𝑥 ∈ ω )
22 nnfi ⊢ ( suc 𝑥 ∈ ω → suc 𝑥 ∈ Fin )
23 diffi ⊢ ( suc 𝑥 ∈ Fin → ( suc 𝑥 ∖ { 𝑦 } ) ∈ Fin )
24 21 22 23 3syl ⊢ ( 𝑥 ∈ ω → ( suc 𝑥 ∖ { 𝑦 } ) ∈ Fin )
25 ssdomfi ⊢ ( ( suc 𝑥 ∖ { 𝑦 } ) ∈ Fin → ( 𝐵 ⊆ ( suc 𝑥 ∖ { 𝑦 } ) → 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) ) )
26 24 25 syl ⊢ ( 𝑥 ∈ ω → ( 𝐵 ⊆ ( suc 𝑥 ∖ { 𝑦 } ) → 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) ) )
27 20 26 sylan9 ⊢ ( ( ¬ 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ω ) → ( 𝐵 ⊊ suc 𝑥 → 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) ) )
28 27 3impia ⊢ ( ( ¬ 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ω ∧ 𝐵 ⊊ suc 𝑥 ) → 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) )
29 28 3com23 ⊢ ( ( ¬ 𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥 ∧ 𝑥 ∈ ω ) → 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) )
30 29 3expa ⊢ ( ( ( ¬ 𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥 ) ∧ 𝑥 ∈ ω ) → 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) )
31 30 adantrr ⊢ ( ( ( ¬ 𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) ) → 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) )
32 nnfi ⊢ ( 𝑥 ∈ ω → 𝑥 ∈ Fin )
33 32 ad2antrl ⊢ ( ( 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) ) → 𝑥 ∈ Fin )
34 simpl ⊢ ( ( 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) ) → 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) )
35 simpr ⊢ ( ( 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) ) → ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) )
36 phplem1 ⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) → 𝑥 ≈ ( suc 𝑥 ∖ { 𝑦 } ) )
37 ensymfib ⊢ ( 𝑥 ∈ Fin → ( 𝑥 ≈ ( suc 𝑥 ∖ { 𝑦 } ) ↔ ( suc 𝑥 ∖ { 𝑦 } ) ≈ 𝑥 ) )
38 32 37 syl ⊢ ( 𝑥 ∈ ω → ( 𝑥 ≈ ( suc 𝑥 ∖ { 𝑦 } ) ↔ ( suc 𝑥 ∖ { 𝑦 } ) ≈ 𝑥 ) )
39 38 adantr ⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) → ( 𝑥 ≈ ( suc 𝑥 ∖ { 𝑦 } ) ↔ ( suc 𝑥 ∖ { 𝑦 } ) ≈ 𝑥 ) )
40 36 39 mpbid ⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) → ( suc 𝑥 ∖ { 𝑦 } ) ≈ 𝑥 )
41 endom ⊢ ( ( suc 𝑥 ∖ { 𝑦 } ) ≈ 𝑥 → ( suc 𝑥 ∖ { 𝑦 } ) ≼ 𝑥 )
42 40 41 syl ⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) → ( suc 𝑥 ∖ { 𝑦 } ) ≼ 𝑥 )
43 domtrfir ⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) ∧ ( suc 𝑥 ∖ { 𝑦 } ) ≼ 𝑥 ) → 𝐵 ≼ 𝑥 )
44 42 43 syl3an3 ⊢ ( ( 𝑥 ∈ Fin ∧ 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) ) → 𝐵 ≼ 𝑥 )
45 33 34 35 44 syl3anc ⊢ ( ( 𝐵 ≼ ( suc 𝑥 ∖ { 𝑦 } ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) ) → 𝐵 ≼ 𝑥 )
46 31 45 sylancom ⊢ ( ( ( ¬ 𝑦 ∈ 𝐵 ∧ 𝐵 ⊊ suc 𝑥 ) ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ suc 𝑥 ) ) → 𝐵 ≼ 𝑥 )
47 46 exp43 ⊢ ( ¬ 𝑦 ∈ 𝐵 → ( 𝐵 ⊊ suc 𝑥 → ( 𝑥 ∈ ω → ( 𝑦 ∈ suc 𝑥 → 𝐵 ≼ 𝑥 ) ) ) )
48 47 com4r ⊢ ( 𝑦 ∈ suc 𝑥 → ( ¬ 𝑦 ∈ 𝐵 → ( 𝐵 ⊊ suc 𝑥 → ( 𝑥 ∈ ω → 𝐵 ≼ 𝑥 ) ) ) )
49 48 imp ⊢ ( ( 𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵 ) → ( 𝐵 ⊊ suc 𝑥 → ( 𝑥 ∈ ω → 𝐵 ≼ 𝑥 ) ) )
50 49 exlimiv ⊢ ( ∃ 𝑦 ( 𝑦 ∈ suc 𝑥 ∧ ¬ 𝑦 ∈ 𝐵 ) → ( 𝐵 ⊊ suc 𝑥 → ( 𝑥 ∈ ω → 𝐵 ≼ 𝑥 ) ) )
51 11 50 mpcom ⊢ ( 𝐵 ⊊ suc 𝑥 → ( 𝑥 ∈ ω → 𝐵 ≼ 𝑥 ) )
52 simp1 ⊢ ( ( 𝑥 ∈ ω ∧ suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥 ) → 𝑥 ∈ ω )
53 endom ⊢ ( suc 𝑥 ≈ 𝐵 → suc 𝑥 ≼ 𝐵 )
54 domtrfir ⊢ ( ( 𝑥 ∈ Fin ∧ suc 𝑥 ≼ 𝐵 ∧ 𝐵 ≼ 𝑥 ) → suc 𝑥 ≼ 𝑥 )
55 53 54 syl3an2 ⊢ ( ( 𝑥 ∈ Fin ∧ suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥 ) → suc 𝑥 ≼ 𝑥 )
56 32 55 syl3an1 ⊢ ( ( 𝑥 ∈ ω ∧ suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥 ) → suc 𝑥 ≼ 𝑥 )
57 sssucid ⊢ 𝑥 ⊆ suc 𝑥
58 ssdomfi ⊢ ( suc 𝑥 ∈ Fin → ( 𝑥 ⊆ suc 𝑥 → 𝑥 ≼ suc 𝑥 ) )
59 22 57 58 mpisyl ⊢ ( suc 𝑥 ∈ ω → 𝑥 ≼ suc 𝑥 )
60 21 59 syl ⊢ ( 𝑥 ∈ ω → 𝑥 ≼ suc 𝑥 )
61 60 adantr ⊢ ( ( 𝑥 ∈ ω ∧ suc 𝑥 ≼ 𝑥 ) → 𝑥 ≼ suc 𝑥 )
62 sbthfi ⊢ ( ( 𝑥 ∈ Fin ∧ suc 𝑥 ≼ 𝑥 ∧ 𝑥 ≼ suc 𝑥 ) → suc 𝑥 ≈ 𝑥 )
63 32 62 syl3an1 ⊢ ( ( 𝑥 ∈ ω ∧ suc 𝑥 ≼ 𝑥 ∧ 𝑥 ≼ suc 𝑥 ) → suc 𝑥 ≈ 𝑥 )
64 61 63 mpd3an3 ⊢ ( ( 𝑥 ∈ ω ∧ suc 𝑥 ≼ 𝑥 ) → suc 𝑥 ≈ 𝑥 )
65 52 56 64 syl2anc ⊢ ( ( 𝑥 ∈ ω ∧ suc 𝑥 ≈ 𝐵 ∧ 𝐵 ≼ 𝑥 ) → suc 𝑥 ≈ 𝑥 )
66 65 3com23 ⊢ ( ( 𝑥 ∈ ω ∧ 𝐵 ≼ 𝑥 ∧ suc 𝑥 ≈ 𝐵 ) → suc 𝑥 ≈ 𝑥 )
67 66 3expia ⊢ ( ( 𝑥 ∈ ω ∧ 𝐵 ≼ 𝑥 ) → ( suc 𝑥 ≈ 𝐵 → suc 𝑥 ≈ 𝑥 ) )
68 peano2b ⊢ ( 𝑥 ∈ ω ↔ suc 𝑥 ∈ ω )
69 nnord ⊢ ( suc 𝑥 ∈ ω → Ord suc 𝑥 )
70 68 69 sylbi ⊢ ( 𝑥 ∈ ω → Ord suc 𝑥 )
71 vex ⊢ 𝑥 ∈ V
72 71 sucid ⊢ 𝑥 ∈ suc 𝑥
73 nordeq ⊢ ( ( Ord suc 𝑥 ∧ 𝑥 ∈ suc 𝑥 ) → suc 𝑥 ≠ 𝑥 )
74 70 72 73 sylancl ⊢ ( 𝑥 ∈ ω → suc 𝑥 ≠ 𝑥 )
75 nneneq ⊢ ( ( suc 𝑥 ∈ ω ∧ 𝑥 ∈ ω ) → ( suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥 ) )
76 68 75 sylanb ⊢ ( ( 𝑥 ∈ ω ∧ 𝑥 ∈ ω ) → ( suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥 ) )
77 76 anidms ⊢ ( 𝑥 ∈ ω → ( suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 = 𝑥 ) )
78 77 necon3bbid ⊢ ( 𝑥 ∈ ω → ( ¬ suc 𝑥 ≈ 𝑥 ↔ suc 𝑥 ≠ 𝑥 ) )
79 74 78 mpbird ⊢ ( 𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝑥 )
80 67 79 nsyli ⊢ ( ( 𝑥 ∈ ω ∧ 𝐵 ≼ 𝑥 ) → ( 𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵 ) )
81 80 expcom ⊢ ( 𝐵 ≼ 𝑥 → ( 𝑥 ∈ ω → ( 𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵 ) ) )
82 81 pm2.43d ⊢ ( 𝐵 ≼ 𝑥 → ( 𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵 ) )
83 51 82 syli ⊢ ( 𝐵 ⊊ suc 𝑥 → ( 𝑥 ∈ ω → ¬ suc 𝑥 ≈ 𝐵 ) )
84 83 com12 ⊢ ( 𝑥 ∈ ω → ( 𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵 ) )
85 psseq2 ⊢ ( 𝐴 = suc 𝑥 → ( 𝐵 ⊊ 𝐴 ↔ 𝐵 ⊊ suc 𝑥 ) )
86 breq1 ⊢ ( 𝐴 = suc 𝑥 → ( 𝐴 ≈ 𝐵 ↔ suc 𝑥 ≈ 𝐵 ) )
87 86 notbid ⊢ ( 𝐴 = suc 𝑥 → ( ¬ 𝐴 ≈ 𝐵 ↔ ¬ suc 𝑥 ≈ 𝐵 ) )
88 85 87 imbi12d ⊢ ( 𝐴 = suc 𝑥 → ( ( 𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵 ) ↔ ( 𝐵 ⊊ suc 𝑥 → ¬ suc 𝑥 ≈ 𝐵 ) ) )
89 84 88 syl5ibrcom ⊢ ( 𝑥 ∈ ω → ( 𝐴 = suc 𝑥 → ( 𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵 ) ) )
90 89 rexlimiv ⊢ ( ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 → ( 𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵 ) )
91 10 90 syl ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ( 𝐵 ⊊ 𝐴 → ¬ 𝐴 ≈ 𝐵 ) )
92 91 syldbl2 ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ¬ 𝐴 ≈ 𝐵 )