Theorem hashnnsuc

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

	Ref	Expression
Assertion	hashnnsuc	$$⊢A\in \mathrm{\omega }\to \left|\mathrm{suc}A\right|=\left|A\right|+1$$

Proof

Step	Hyp	Ref	Expression
1		nnon	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{On}$$
2		oa1suc	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}{1}_{𝑜}=\mathrm{suc}A$$
3	1 2	syl	$$⊢A\in \mathrm{\omega }\to A{+}_{𝑜}{1}_{𝑜}=\mathrm{suc}A$$
4	3	fveq2d	$$⊢A\in \mathrm{\omega }\to \left|A{+}_{𝑜}{1}_{𝑜}\right|=\left|\mathrm{suc}A\right|$$
5		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
6		hashnna	$$⊢\left(A\in \mathrm{\omega }\wedge 1_{𝑜}\in \mathrm{\omega }\right)\to \left|A{+}_{𝑜}{1}_{𝑜}\right|=\left|A\right|+\left|1_{𝑜}\right|$$
7	5 6	mpan2	$$⊢A\in \mathrm{\omega }\to \left|A{+}_{𝑜}{1}_{𝑜}\right|=\left|A\right|+\left|1_{𝑜}\right|$$
8	4 7	eqtr3d	$$⊢A\in \mathrm{\omega }\to \left|\mathrm{suc}A\right|=\left|A\right|+\left|1_{𝑜}\right|$$
9		hash1	$$⊢\left|1_{𝑜}\right|=1$$
10	9	oveq2i	$$⊢\left|A\right|+\left|1_{𝑜}\right|=\left|A\right|+1$$
11	8 10	eqtrdi	$$⊢A\in \mathrm{\omega }\to \left|\mathrm{suc}A\right|=\left|A\right|+1$$