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	$$⊢\left(x\in ℂ,y\in ℂ⟼x+y\right):ℂ\times ℂ⟶ℂ$$

Proof

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