Theorem phplem3

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)

	Ref	Expression
Hypotheses	phplem2.1	|- A e. _V
	phplem2.2	|- B e. _V
Assertion	phplem3	|- ( ( A e. _om /\ B e. suc A ) -> A ~~ ( suc A \ { B } ) )

Proof

Step	Hyp	Ref	Expression
1		phplem2.1	|- A e. _V
2		phplem2.2	|- B e. _V
3		elsuci	|- ( B e. suc A -> ( B e. A \/ B = A ) )
4	1 2	phplem2	|- ( ( A e. _om /\ B e. A ) -> A ~~ ( suc A \ { B } ) )
5	1	enref	|- A ~~ A
6		nnord	|- ( A e. _om -> Ord A )
7		orddif	|- ( Ord A -> A = ( suc A \ { A } ) )
8	6 7	syl	|- ( A e. _om -> A = ( suc A \ { A } ) )
9		sneq	|- ( A = B -> { A } = { B } )
10	9	difeq2d	|- ( A = B -> ( suc A \ { A } ) = ( suc A \ { B } ) )
11	10	eqcoms	|- ( B = A -> ( suc A \ { A } ) = ( suc A \ { B } ) )
12	8 11	sylan9eq	|- ( ( A e. _om /\ B = A ) -> A = ( suc A \ { B } ) )
13	5 12	breqtrid	|- ( ( A e. _om /\ B = A ) -> A ~~ ( suc A \ { B } ) )
14	4 13	jaodan	|- ( ( A e. _om /\ ( B e. A \/ B = A ) ) -> A ~~ ( suc A \ { B } ) )
15	3 14	sylan2	|- ( ( A e. _om /\ B e. suc A ) -> A ~~ ( suc A \ { B } ) )