hashnna

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

		Ref	Expression
	Assertion	hashnna	$⊢ (A \in ω \land B \in ω) \to \|A +_{𝑜} B\| = \|A\| + \|B\|$

Step	Hyp	Ref	Expression
1		hashgval2	$⊢ {\|.\| ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
2	1	hashgadd	$⊢ (A \in ω \land B \in ω) \to ({\|.\| ↾}_{ω}) (A +_{𝑜} B) = ({\|.\| ↾}_{ω}) (A) + ({\|.\| ↾}_{ω}) (B)$
3		nnacl	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} B \in ω$
4	3	fvresd	$⊢ (A \in ω \land B \in ω) \to ({\|.\| ↾}_{ω}) (A +_{𝑜} B) = \|A +_{𝑜} B\|$
5		fvres	$⊢ A \in ω \to ({\|.\| ↾}_{ω}) (A) = \|A\|$
6		fvres	$⊢ B \in ω \to ({\|.\| ↾}_{ω}) (B) = \|B\|$
7	5 6	oveqan12d	$⊢ (A \in ω \land B \in ω) \to ({\|.\| ↾}_{ω}) (A) + ({\|.\| ↾}_{ω}) (B) = \|A\| + \|B\|$
8	2 4 7	3eqtr3d	$⊢ (A \in ω \land B \in ω) \to \|A +_{𝑜} B\| = \|A\| + \|B\|$

Metamath Proof Explorer