This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmmulpi

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

Ref Expression
Assertion dmmulpi dom ·N = ( N × N )

Proof

Step Hyp Ref Expression
1 dmres ⊢ dom ( ·o ↾ ( N × N ) ) = ( ( N × N ) ∩ dom ·o )
2 fnom ⊢ ·o Fn ( On × On )
3 2 fndmi ⊢ dom ·o = ( On × On )
4 3 ineq2i ⊢ ( ( N × N ) ∩ dom ·o ) = ( ( N × N ) ∩ ( On × On ) )
5 1 4 eqtri ⊢ dom ( ·o ↾ ( N × N ) ) = ( ( N × N ) ∩ ( On × On ) )
6 df-mi ⊢ ·N = ( ·o ↾ ( N × N ) )
7 6 dmeqi ⊢ dom ·N = dom ( ·o ↾ ( N × N ) )
8 df-ni ⊢ N = ( ω ∖ { ∅ } )
9 difss ⊢ ( ω ∖ { ∅ } ) ⊆ ω
10 8 9 eqsstri ⊢ N ⊆ ω
11 omsson ⊢ ω ⊆ On
12 10 11 sstri ⊢ N ⊆ On
13 anidm ⊢ ( ( N ⊆ On ∧ N ⊆ On ) ↔ N ⊆ On )
14 12 13 mpbir ⊢ ( N ⊆ On ∧ N ⊆ On )
15 xpss12 ⊢ ( ( N ⊆ On ∧ N ⊆ On ) → ( N × N ) ⊆ ( On × On ) )
16 14 15 ax-mp ⊢ ( N × N ) ⊆ ( On × On )
17 dfss ⊢ ( ( N × N ) ⊆ ( On × On ) ↔ ( N × N ) = ( ( N × N ) ∩ ( On × On ) ) )
18 16 17 mpbi ⊢ ( N × N ) = ( ( N × N ) ∩ ( On × On ) )
19 5 7 18 3eqtr4i ⊢ dom ·N = ( N × N )