Metamath Proof Explorer


Theorem dmaddpi

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

Ref Expression
Assertion dmaddpi dom +N = ( N × N )

Proof

Step Hyp Ref Expression
1 dmres dom ( +o ↾ ( N × N ) ) = ( ( N × N ) ∩ dom +o )
2 fnoa +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-pli +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 )