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. X. N. )

Proof

Step Hyp Ref Expression
1 dmres
 |-  dom ( +o |` ( N. X. N. ) ) = ( ( N. X. N. ) i^i dom +o )
2 fnoa
 |-  +o Fn ( On X. On )
3 2 fndmi
 |-  dom +o = ( On X. On )
4 3 ineq2i
 |-  ( ( N. X. N. ) i^i dom +o ) = ( ( N. X. N. ) i^i ( On X. On ) )
5 1 4 eqtri
 |-  dom ( +o |` ( N. X. N. ) ) = ( ( N. X. N. ) i^i ( On X. On ) )
6 df-pli
 |-  +N = ( +o |` ( N. X. N. ) )
7 6 dmeqi
 |-  dom +N = dom ( +o |` ( N. X. N. ) )
8 df-ni
 |-  N. = ( _om \ { (/) } )
9 difss
 |-  ( _om \ { (/) } ) C_ _om
10 8 9 eqsstri
 |-  N. C_ _om
11 omsson
 |-  _om C_ On
12 10 11 sstri
 |-  N. C_ On
13 anidm
 |-  ( ( N. C_ On /\ N. C_ On ) <-> N. C_ On )
14 12 13 mpbir
 |-  ( N. C_ On /\ N. C_ On )
15 xpss12
 |-  ( ( N. C_ On /\ N. C_ On ) -> ( N. X. N. ) C_ ( On X. On ) )
16 14 15 ax-mp
 |-  ( N. X. N. ) C_ ( On X. On )
17 dfss
 |-  ( ( N. X. N. ) C_ ( On X. On ) <-> ( N. X. N. ) = ( ( N. X. N. ) i^i ( On X. On ) ) )
18 16 17 mpbi
 |-  ( N. X. N. ) = ( ( N. X. N. ) i^i ( On X. On ) )
19 5 7 18 3eqtr4i
 |-  dom +N = ( N. X. N. )