Metamath Proof Explorer


Theorem phplem1

Description: Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus any element of the successor. (Contributed by NM, 26-May-1998) Avoid ax-pow . (Revised by BTernaryTau, 23-Sep-2024)

Ref Expression
Assertion phplem1 AωBsucAAsucAB

Proof

Step Hyp Ref Expression
1 simpl AωBsucAAω
2 peano2 AωsucAω
3 enrefnn sucAωsucAsucA
4 2 3 syl AωsucAsucA
5 4 adantr AωBsucAsucAsucA
6 simpr AωBsucABsucA
7 dif1en AωsucAsucABsucAsucABA
8 1 5 6 7 syl3anc AωBsucAsucABA
9 nnfi AωAFin
10 ensymfib AFinAsucABsucABA
11 1 9 10 3syl AωBsucAAsucABsucABA
12 8 11 mpbird AωBsucAAsucAB