This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mpoaddf

Description: Addition is an operation on complex numbers. Version of ax-addf using maps-to notation, proved from the axioms of set theory and ax-addcl . (Contributed by GG, 31-Mar-2025)

		Ref	Expression
	Assertion	mpoaddf	$⊢ (x \in ℂ, y \in ℂ ⟼ x + y) : ℂ \times ℂ ⟶ ℂ$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (x \in ℂ, y \in ℂ ⟼ x + y) = (x \in ℂ, y \in ℂ ⟼ x + y)$
2		ovex	$⊢ x + y \in V$
3	1 2	fnmpoi	$⊢ (x \in ℂ, y \in ℂ ⟼ x + y) Fn (ℂ \times ℂ)$
4		simpll	$⊢ ((x \in ℂ \land y \in ℂ) \land z = x + y) \to x \in ℂ$
5		simplr	$⊢ ((x \in ℂ \land y \in ℂ) \land z = x + y) \to y \in ℂ$
6		addcl	$⊢ (x \in ℂ \land y \in ℂ) \to x + y \in ℂ$
7		eleq1a	$⊢ x + y \in ℂ \to (z = x + y \to z \in ℂ)$
8	6 7	syl	$⊢ (x \in ℂ \land y \in ℂ) \to (z = x + y \to z \in ℂ)$
9	8	imp	$⊢ ((x \in ℂ \land y \in ℂ) \land z = x + y) \to z \in ℂ$
10	4 5 9	3jca	$⊢ ((x \in ℂ \land y \in ℂ) \land z = x + y) \to (x \in ℂ \land y \in ℂ \land z \in ℂ)$
11	10	ssoprab2i	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in ℂ \land y \in ℂ) \land z = x + y)\} \subseteq \{⟨⟨x, y⟩, z⟩ \| (x \in ℂ \land y \in ℂ \land z \in ℂ)\}$
12		df-mpo	$⊢ (x \in ℂ, y \in ℂ ⟼ x + y) = \{⟨⟨x, y⟩, z⟩ \| ((x \in ℂ \land y \in ℂ) \land z = x + y)\}$
13		dfxp3	$⊢ (ℂ \times ℂ) \times ℂ = \{⟨⟨x, y⟩, z⟩ \| (x \in ℂ \land y \in ℂ \land z \in ℂ)\}$
14	11 12 13	3sstr4i	$⊢ (x \in ℂ, y \in ℂ ⟼ x + y) \subseteq (ℂ \times ℂ) \times ℂ$
15		dff2	$⊢ (x \in ℂ, y \in ℂ ⟼ x + y) : ℂ \times ℂ ⟶ ℂ \leftrightarrow ((x \in ℂ, y \in ℂ ⟼ x + y) Fn (ℂ \times ℂ) \land (x \in ℂ, y \in ℂ ⟼ x + y) \subseteq (ℂ \times ℂ) \times ℂ)$
16	3 14 15	mpbir2an	$⊢ (x \in ℂ, y \in ℂ ⟼ x + y) : ℂ \times ℂ ⟶ ℂ$