This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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