Metamath Proof Explorer

Theorem mpomulf

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

		Ref	Expression
	Assertion	mpomulf	$⊢ (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		mulcl	$⊢ (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 ℂ ⟶ ℂ$