Theorem dmaddpi

Description: Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	dmaddpi	$$⊢\mathrm{dom}{+}_{𝑵}=𝑵\times 𝑵$$

Proof

Step	Hyp	Ref	Expression
1		dmres	$$⊢\mathrm{dom}\left({{+}_{𝑜}\upharpoonright }_{\left(𝑵\times 𝑵\right)}\right)=\left(𝑵\times 𝑵\right)\cap \mathrm{dom}{+}_{𝑜}$$
2		fnoa	$$⊢{+}_{𝑜}Fn\left(\mathrm{On}\times \mathrm{On}\right)$$
3	2	fndmi	$$⊢\mathrm{dom}{+}_{𝑜}=\mathrm{On}\times \mathrm{On}$$
4	3	ineq2i	$$⊢\left(𝑵\times 𝑵\right)\cap \mathrm{dom}{+}_{𝑜}=\left(𝑵\times 𝑵\right)\cap \left(\mathrm{On}\times \mathrm{On}\right)$$
5	1 4	eqtri	$$⊢\mathrm{dom}\left({{+}_{𝑜}\upharpoonright }_{\left(𝑵\times 𝑵\right)}\right)=\left(𝑵\times 𝑵\right)\cap \left(\mathrm{On}\times \mathrm{On}\right)$$
6		df-pli	$$⊢{+}_{𝑵}={{+}_{𝑜}\upharpoonright }_{\left(𝑵\times 𝑵\right)}$$
7	6	dmeqi	$$⊢\mathrm{dom}{+}_{𝑵}=\mathrm{dom}\left({{+}_{𝑜}\upharpoonright }_{\left(𝑵\times 𝑵\right)}\right)$$
8		df-ni	$$⊢𝑵=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
9		difss	$$⊢\mathrm{\omega }\setminus \left\{\varnothing \right\}\subseteq \mathrm{\omega }$$
10	8 9	eqsstri	$$⊢𝑵\subseteq \mathrm{\omega }$$
11		omsson	$$⊢\mathrm{\omega }\subseteq \mathrm{On}$$
12	10 11	sstri	$$⊢𝑵\subseteq \mathrm{On}$$
13		anidm	$$⊢\left(𝑵\subseteq \mathrm{On}\wedge 𝑵\subseteq \mathrm{On}\right)\leftrightarrow 𝑵\subseteq \mathrm{On}$$
14	12 13	mpbir	$$⊢\left(𝑵\subseteq \mathrm{On}\wedge 𝑵\subseteq \mathrm{On}\right)$$
15		xpss12	$$⊢\left(𝑵\subseteq \mathrm{On}\wedge 𝑵\subseteq \mathrm{On}\right)\to 𝑵\times 𝑵\subseteq \mathrm{On}\times \mathrm{On}$$
16	14 15	ax-mp	$$⊢𝑵\times 𝑵\subseteq \mathrm{On}\times \mathrm{On}$$
17		dfss	$$⊢𝑵\times 𝑵\subseteq \mathrm{On}\times \mathrm{On}\leftrightarrow 𝑵\times 𝑵=\left(𝑵\times 𝑵\right)\cap \left(\mathrm{On}\times \mathrm{On}\right)$$
18	16 17	mpbi	$$⊢𝑵\times 𝑵=\left(𝑵\times 𝑵\right)\cap \left(\mathrm{On}\times \mathrm{On}\right)$$
19	5 7 18	3eqtr4i	$$⊢\mathrm{dom}{+}_{𝑵}=𝑵\times 𝑵$$