Theorem hashnnsuc

Description: The # function on _om turns successor into adding 1. (Contributed by Eric Schmidt, 7-Jul-2026)

	Ref	Expression
Assertion	hashnnsuc	⊢ ( 𝐴 ∈ ω → ( ♯ ‘ suc 𝐴 ) = ( ( ♯ ‘ 𝐴 ) + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
2		oa1suc	⊢ ( 𝐴 ∈ On → ( 𝐴 +o 1o ) = suc 𝐴 )
3	1 2	syl	⊢ ( 𝐴 ∈ ω → ( 𝐴 +o 1o ) = suc 𝐴 )
4	3	fveq2d	⊢ ( 𝐴 ∈ ω → ( ♯ ‘ ( 𝐴 +o 1o ) ) = ( ♯ ‘ suc 𝐴 ) )
5		1onn	⊢ 1o ∈ ω
6		hashnna	⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ ω ) → ( ♯ ‘ ( 𝐴 +o 1o ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 1o ) ) )
7	5 6	mpan2	⊢ ( 𝐴 ∈ ω → ( ♯ ‘ ( 𝐴 +o 1o ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 1o ) ) )
8	4 7	eqtr3d	⊢ ( 𝐴 ∈ ω → ( ♯ ‘ suc 𝐴 ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 1o ) ) )
9		hash1	⊢ ( ♯ ‘ 1o ) = 1
10	9	oveq2i	⊢ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 1o ) ) = ( ( ♯ ‘ 𝐴 ) + 1 )
11	8 10	eqtrdi	⊢ ( 𝐴 ∈ ω → ( ♯ ‘ suc 𝐴 ) = ( ( ♯ ‘ 𝐴 ) + 1 ) )