naddf

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

		Ref	Expression
	Assertion	naddf	$⊢ + : On \times On ⟶ On$

Step	Hyp	Ref	Expression
1		naddfn	$⊢ + Fn (On \times On)$
2		naddcl	$⊢ (y \in On \land z \in On) \to y + z \in On$
3	2	rgen2	$⊢ \forall y \in On \forall z \in On y + z \in On$
4		fveq2	$⊢ x = ⟨y, z⟩ \to + (x) = + (⟨y, z⟩)$
5		df-ov	$⊢ y + z = + (⟨y, z⟩)$
6	4 5	eqtr4di	$⊢ x = ⟨y, z⟩ \to + (x) = y + z$
7	6	eleq1d	$⊢ x = ⟨y, z⟩ \to (+ (x) \in On \leftrightarrow y + z \in On)$
8	7	ralxp	$⊢ \forall x \in (On \times On) + (x) \in On \leftrightarrow \forall y \in On \forall z \in On y + z \in On$
9	3 8	mpbir	$⊢ \forall x \in (On \times On) + (x) \in On$
10		ffnfv	$⊢ + : On \times On ⟶ On \leftrightarrow (+ Fn (On \times On) \land \forall x \in (On \times On) + (x) \in On)$
11	1 9 10	mpbir2an	$⊢ + : On \times On ⟶ On$

Metamath Proof Explorer