Metamath Proof Explorer


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 } )