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 ( 𝐴 ∈ ω → ( har ‘ 𝐴 ) = suc 𝐴 )

Proof

Step Hyp Ref Expression
1 nnon ( 𝐴 ∈ ω → 𝐴 ∈ On )
2 onenon ( 𝐴 ∈ On → 𝐴 ∈ dom card )
3 harval2 ( 𝐴 ∈ dom card → ( har ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝐴𝑥 } )
4 1 2 3 3syl ( 𝐴 ∈ ω → ( har ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝐴𝑥 } )
5 sucdom ( 𝐴 ∈ ω → ( 𝐴𝑥 ↔ suc 𝐴𝑥 ) )
6 5 adantr ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ On ) → ( 𝐴𝑥 ↔ suc 𝐴𝑥 ) )
7 peano2 ( 𝐴 ∈ ω → suc 𝐴 ∈ ω )
8 nndomog ( ( suc 𝐴 ∈ ω ∧ 𝑥 ∈ On ) → ( suc 𝐴𝑥 ↔ suc 𝐴𝑥 ) )
9 7 8 sylan ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ On ) → ( suc 𝐴𝑥 ↔ suc 𝐴𝑥 ) )
10 6 9 bitrd ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ On ) → ( 𝐴𝑥 ↔ suc 𝐴𝑥 ) )
11 10 rabbidva ( 𝐴 ∈ ω → { 𝑥 ∈ On ∣ 𝐴𝑥 } = { 𝑥 ∈ On ∣ suc 𝐴𝑥 } )
12 11 inteqd ( 𝐴 ∈ ω → { 𝑥 ∈ On ∣ 𝐴𝑥 } = { 𝑥 ∈ On ∣ suc 𝐴𝑥 } )
13 nnon ( suc 𝐴 ∈ ω → suc 𝐴 ∈ On )
14 intmin ( suc 𝐴 ∈ On → { 𝑥 ∈ On ∣ suc 𝐴𝑥 } = suc 𝐴 )
15 7 13 14 3syl ( 𝐴 ∈ ω → { 𝑥 ∈ On ∣ suc 𝐴𝑥 } = suc 𝐴 )
16 4 12 15 3eqtrd ( 𝐴 ∈ ω → ( har ‘ 𝐴 ) = suc 𝐴 )