Theorem onsucmin

Description: The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003)

	Ref	Expression
Assertion	onsucmin	|- ( A e. On -> suc A = |^| { x e. On | A e. x } )

Proof

Step	Hyp	Ref	Expression
1		eloni	|- ( x e. On -> Ord x )
2		ordelsuc	|- ( ( A e. On /\ Ord x ) -> ( A e. x <-> suc A C_ x ) )
3	1 2	sylan2	|- ( ( A e. On /\ x e. On ) -> ( A e. x <-> suc A C_ x ) )
4	3	rabbidva	|- ( A e. On -> { x e. On | A e. x } = { x e. On | suc A C_ x } )
5	4	inteqd	|- ( A e. On -> |^| { x e. On | A e. x } = |^| { x e. On | suc A C_ x } )
6		sucelon	|- ( A e. On <-> suc A e. On )
7		intmin	|- ( suc A e. On -> |^| { x e. On | suc A C_ x } = suc A )
8	6 7	sylbi	|- ( A e. On -> |^| { x e. On | suc A C_ x } = suc A )
9	5 8	eqtr2d	|- ( A e. On -> suc A = |^| { x e. On | A e. x } )