Theorem fin1a2lem1

Description: Lemma for fin1a2 . (Contributed by Stefan O'Rear, 7-Nov-2014)

	Ref	Expression
Hypothesis	fin1a2lem.a	|- S = ( x e. On |-> suc x )
Assertion	fin1a2lem1	|- ( A e. On -> ( S ` A ) = suc A )

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.a	|- S = ( x e. On |-> suc x )
2		onsuc	|- ( A e. On -> suc A e. On )
3		suceq	|- ( a = A -> suc a = suc A )
4		suceq	|- ( x = a -> suc x = suc a )
5	4	cbvmptv	|- ( x e. On |-> suc x ) = ( a e. On |-> suc a )
6	1 5	eqtri	|- S = ( a e. On |-> suc a )
7	3 6	fvmptg	|- ( ( A e. On /\ suc A e. On ) -> ( S ` A ) = suc A )
8	2 7	mpdan	|- ( A e. On -> ( S ` A ) = suc A )