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 e. _om /\ B e. suc A ) -> A ~~ ( suc A \ { B } ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A e. _om /\ B e. suc A ) -> A e. _om )
2		peano2	|- ( A e. _om -> suc A e. _om )
3		enrefnn	|- ( suc A e. _om -> suc A ~~ suc A )
4	2 3	syl	|- ( A e. _om -> suc A ~~ suc A )
5	4	adantr	|- ( ( A e. _om /\ B e. suc A ) -> suc A ~~ suc A )
6		simpr	|- ( ( A e. _om /\ B e. suc A ) -> B e. suc A )
7		dif1ennn	|- ( ( A e. _om /\ suc A ~~ suc A /\ B e. suc A ) -> ( suc A \ { B } ) ~~ A )
8	1 5 6 7	syl3anc	|- ( ( A e. _om /\ B e. suc A ) -> ( suc A \ { B } ) ~~ A )
9		nnfi	|- ( A e. _om -> A e. Fin )
10		ensymfib	|- ( A e. Fin -> ( A ~~ ( suc A \ { B } ) <-> ( suc A \ { B } ) ~~ A ) )
11	1 9 10	3syl	|- ( ( A e. _om /\ B e. suc A ) -> ( A ~~ ( suc A \ { B } ) <-> ( suc A \ { B } ) ~~ A ) )
12	8 11	mpbird	|- ( ( A e. _om /\ B e. suc A ) -> A ~~ ( suc A \ { B } ) )