Theorem naddf

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

	Ref	Expression
Assertion	naddf	Could not format assertion : No typesetting found for |- +no : ( On X. On ) --> On with typecode |-

Proof

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