Theorem hashnna

Description: The # function on _om preserves addition. (Contributed by Eric Schmidt, 7-Jul-2026)

	Ref	Expression
Assertion	hashnna	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ♯ ‘ ( 𝐴 +o 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hashgval2	⊢ ( ♯ ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
2	1	hashgadd	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( ♯ ↾ ω ) ‘ ( 𝐴 +o 𝐵 ) ) = ( ( ( ♯ ↾ ω ) ‘ 𝐴 ) + ( ( ♯ ↾ ω ) ‘ 𝐵 ) ) )
3		nnacl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) ∈ ω )
4	3	fvresd	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( ♯ ↾ ω ) ‘ ( 𝐴 +o 𝐵 ) ) = ( ♯ ‘ ( 𝐴 +o 𝐵 ) ) )
5		fvres	⊢ ( 𝐴 ∈ ω → ( ( ♯ ↾ ω ) ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) )
6		fvres	⊢ ( 𝐵 ∈ ω → ( ( ♯ ↾ ω ) ‘ 𝐵 ) = ( ♯ ‘ 𝐵 ) )
7	5 6	oveqan12d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( ( ♯ ↾ ω ) ‘ 𝐴 ) + ( ( ♯ ↾ ω ) ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
8	2 4 7	3eqtr3d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ♯ ‘ ( 𝐴 +o 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )