Metamath Proof Explorer

Theorem naddf

Description: Function statement for natural addition. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Assertion naddf 
|- +no : ( On X. On ) --> On

Proof

Step Hyp Ref Expression
1 naddfn 
 |-  +no Fn ( On X. On )
2 naddcl 
 |-  ( ( y e. On /\ z e. On ) -> ( y +no z ) e. On )
3 2 rgen2 
 |-  A. y e. On A. z e. On ( y +no z ) e. On
4 fveq2 
 |-  ( x = <. y , z >. -> ( +no ` x ) = ( +no ` <. y , z >. ) )
5 df-ov 
 |-  ( y +no z ) = ( +no ` <. y , z >. )
6 4 5 eqtr4di 
 |-  ( x = <. y , z >. -> ( +no ` x ) = ( y +no z ) )
7 6 eleq1d 
 |-  ( x = <. y , z >. -> ( ( +no ` x ) e. On <-> ( y +no z ) e. On ) )
8 7 ralxp 
 |-  ( A. x e. ( On X. On ) ( +no ` x ) e. On <-> A. y e. On A. z e. On ( y +no z ) e. On )
9 3 8 mpbir 
 |-  A. x e. ( On X. On ) ( +no ` x ) e. On
10 ffnfv 
 |-  ( +no : ( On X. On ) --> On <-> ( +no Fn ( On X. On ) /\ A. x e. ( On X. On ) ( +no ` x ) e. On ) )
11 1 9 10 mpbir2an 
 |-  +no : ( On X. On ) --> On