Metamath Proof Explorer


Theorem phplem1

Description: Lemma for Pigeonhole Principle. If we join a natural number to itself minus an element, we end up with its successor minus the same element. (Contributed by NM, 25-May-1998)

Ref Expression
Assertion phplem1 A ω B A A A B = suc A B

Proof

Step Hyp Ref Expression
1 nnord A ω Ord A
2 nordeq Ord A B A A B
3 disjsn2 A B A B =
4 2 3 syl Ord A B A A B =
5 1 4 sylan A ω B A A B =
6 undif4 A B = A A B = A A B
7 df-suc suc A = A A
8 7 equncomi suc A = A A
9 8 difeq1i suc A B = A A B
10 6 9 eqtr4di A B = A A B = suc A B
11 5 10 syl A ω B A A A B = suc A B