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