Metamath Proof Explorer

Theorem harsucnn

Description: The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023)

Ref Expression
Assertion harsucnn 
|- ( A e. _om -> ( har ` A ) = suc A )

Proof

Step Hyp Ref Expression
1 nnon 
 |-  ( A e. _om -> A e. On )
2 onenon 
 |-  ( A e. On -> A e. dom card )
3 harval2 
 |-  ( A e. dom card -> ( har ` A ) = |^| { x e. On | A ~< x } )
4 1 2 3 3syl 
 |-  ( A e. _om -> ( har ` A ) = |^| { x e. On | A ~< x } )
5 sucdom 
 |-  ( A e. _om -> ( A ~< x <-> suc A ~<_ x ) )
6 5 adantr 
 |-  ( ( A e. _om /\ x e. On ) -> ( A ~< x <-> suc A ~<_ x ) )
7 peano2 
 |-  ( A e. _om -> suc A e. _om )
8 nndomog 
 |-  ( ( suc A e. _om /\ x e. On ) -> ( suc A ~<_ x <-> suc A C_ x ) )
9 7 8 sylan 
 |-  ( ( A e. _om /\ x e. On ) -> ( suc A ~<_ x <-> suc A C_ x ) )
10 6 9 bitrd 
 |-  ( ( A e. _om /\ x e. On ) -> ( A ~< x <-> suc A C_ x ) )
11 10 rabbidva 
 |-  ( A e. _om -> { x e. On | A ~< x } = { x e. On | suc A C_ x } )
12 11 inteqd 
 |-  ( A e. _om -> |^| { x e. On | A ~< x } = |^| { x e. On | suc A C_ x } )
13 nnon 
 |-  ( suc A e. _om -> suc A e. On )
14 intmin 
 |-  ( suc A e. On -> |^| { x e. On | suc A C_ x } = suc A )
15 7 13 14 3syl 
 |-  ( A e. _om -> |^| { x e. On | suc A C_ x } = suc A )
16 4 12 15 3eqtrd 
 |-  ( A e. _om -> ( har ` A ) = suc A )