Theorem phplem3OLD

Description: Obsolete version of phplem1 as of 4-Nov-2024. (Contributed by NM, 26-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		phplem2OLD.1	|- A e. _V
2		phplem2OLD.2	|- B e. _V
3		elsuci	|- ( B e. suc A -> ( B e. A \/ B = A ) )
4	1 2	phplem2OLD	|- ( ( 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 } ) )