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	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) )
2		ovex	⊢ ( 𝑥 · 𝑦 ) ∈ V
3	1 2	fnmpoi	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) Fn ( ℂ × ℂ )
4		simpll	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ 𝑧 = ( 𝑥 · 𝑦 ) ) → 𝑥 ∈ ℂ )
5		simplr	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ 𝑧 = ( 𝑥 · 𝑦 ) ) → 𝑦 ∈ ℂ )
6		mulcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
7		eleq1a	⊢ ( ( 𝑥 · 𝑦 ) ∈ ℂ → ( 𝑧 = ( 𝑥 · 𝑦 ) → 𝑧 ∈ ℂ ) )
8	6 7	syl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑧 = ( 𝑥 · 𝑦 ) → 𝑧 ∈ ℂ ) )
9	8	imp	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ 𝑧 = ( 𝑥 · 𝑦 ) ) → 𝑧 ∈ ℂ )
10	4 5 9	3jca	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ 𝑧 = ( 𝑥 · 𝑦 ) ) → ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) )
11	10	ssoprab2i	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ 𝑧 = ( 𝑥 · 𝑦 ) ) } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) }
12		df-mpo	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ 𝑧 = ( 𝑥 · 𝑦 ) ) }
13		dfxp3	⊢ ( ( ℂ × ℂ ) × ℂ ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) }
14	11 12 13	3sstr4i	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( ( ℂ × ℂ ) × ℂ )
15		dff2	⊢ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ ↔ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) Fn ( ℂ × ℂ ) ∧ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⊆ ( ( ℂ × ℂ ) × ℂ ) ) )
16	3 14 15	mpbir2an	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ