Theorem dmmulpi

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

	Ref	Expression
Assertion	dmmulpi	$$⊢\mathrm{dom}{\cdot }_{𝑵}=𝑵\times 𝑵$$

Proof

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