dmmulpi

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

		Ref	Expression
	Assertion	dmmulpi	$⊢ dom \cdot_{𝑵} = 𝑵 \times 𝑵$

Step	Hyp	Ref	Expression
1		dmres	$⊢ dom ({\cdot_{𝑜} ↾}_{(𝑵 \times 𝑵)}) = (𝑵 \times 𝑵) \cap dom \cdot_{𝑜}$
2		fnom	$⊢ \cdot_{𝑜} Fn (On \times On)$
3	2	fndmi	$⊢ dom \cdot_{𝑜} = On \times On$
4	3	ineq2i	$⊢ (𝑵 \times 𝑵) \cap dom \cdot_{𝑜} = (𝑵 \times 𝑵) \cap (On \times On)$
5	1 4	eqtri	$⊢ dom ({\cdot_{𝑜} ↾}_{(𝑵 \times 𝑵)}) = (𝑵 \times 𝑵) \cap (On \times On)$
6		df-mi	$⊢ \cdot_{𝑵} = {\cdot_{𝑜} ↾}_{(𝑵 \times 𝑵)}$
7	6	dmeqi	$⊢ dom \cdot_{𝑵} = dom ({\cdot_{𝑜} ↾}_{(𝑵 \times 𝑵)})$
8		df-ni	$⊢ 𝑵 = ω ∖ \{\emptyset\}$
9		difss	$⊢ ω ∖ \{\emptyset\} \subseteq ω$
10	8 9	eqsstri	$⊢ 𝑵 \subseteq ω$
11		omsson	$⊢ ω \subseteq On$
12	10 11	sstri	$⊢ 𝑵 \subseteq On$
13		anidm	$⊢ (𝑵 \subseteq On \land 𝑵 \subseteq On) \leftrightarrow 𝑵 \subseteq On$
14	12 13	mpbir	$⊢ (𝑵 \subseteq On \land 𝑵 \subseteq On)$
15		xpss12	$⊢ (𝑵 \subseteq On \land 𝑵 \subseteq On) \to 𝑵 \times 𝑵 \subseteq On \times On$
16	14 15	ax-mp	$⊢ 𝑵 \times 𝑵 \subseteq On \times On$
17		dfss	$⊢ 𝑵 \times 𝑵 \subseteq On \times On \leftrightarrow 𝑵 \times 𝑵 = (𝑵 \times 𝑵) \cap (On \times On)$
18	16 17	mpbi	$⊢ 𝑵 \times 𝑵 = (𝑵 \times 𝑵) \cap (On \times On)$
19	5 7 18	3eqtr4i	$⊢ dom \cdot_{𝑵} = 𝑵 \times 𝑵$

Metamath Proof Explorer