Theorem naddcnffn

Description: Addition operator for Cantor normal forms is a function. (Contributed by RP, 2-Jan-2025)

	Ref	Expression
Assertion	naddcnffn	$$⊢\left(X\in \mathrm{On}\wedge S=\mathrm{dom}\left(\mathrm{\omega }\mathrm{CNF}X\right)\right)\to \left({{\circ }_f{+}_{𝑜}\upharpoonright }_{\left(S\times S\right)}\right)Fn\left(S\times S\right)$$

Proof

Step	Hyp	Ref	Expression
1		naddcnff	$$⊢\left(X\in \mathrm{On}\wedge S=\mathrm{dom}\left(\mathrm{\omega }\mathrm{CNF}X\right)\right)\to \left({{\circ }_f{+}_{𝑜}\upharpoonright }_{\left(S\times S\right)}\right):S\times S⟶S$$
2	1	ffnd	$$⊢\left(X\in \mathrm{On}\wedge S=\mathrm{dom}\left(\mathrm{\omega }\mathrm{CNF}X\right)\right)\to \left({{\circ }_f{+}_{𝑜}\upharpoonright }_{\left(S\times S\right)}\right)Fn\left(S\times S\right)$$