Theorem naddfn

Description: Natural addition is a function over pairs of ordinals. (Contributed by Scott Fenton, 26-Aug-2024)

	Ref	Expression
Assertion	naddfn	$$⊢+Fn\left(\mathrm{On}\times \mathrm{On}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-nadd	$$⊢+=\mathrm{frecs}\left(\left\{⟨x,y⟩|\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge \left(\left(1^{st}\left(x\right)\mathrm{E}{1}^{st}\left(y\right)\vee 1^{st}\left(x\right)=1^{st}\left(y\right)\right)\wedge \left(2^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\wedge x\ne y\right)\right)\right\},\mathrm{On}\times \mathrm{On},\left(z\in \mathrm{V},a\in \mathrm{V}⟼\bigcap \left\{w\in \mathrm{On}|\left(a\left[\left\{1^{st}\left(z\right)\right\}\times 2^{nd}\left(z\right)\right]\subseteq w\wedge a\left[1^{st}\left(z\right)\times \left\{2^{nd}\left(z\right)\right\}\right]\subseteq w\right)\right\}\right)\right)$$
2	1	on2recsfn	$$⊢+Fn\left(\mathrm{On}\times \mathrm{On}\right)$$