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

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) )
2 ovex ⊢ ( 𝑥 + 𝑦 ) ∈ V
3 1 2 fnmpoi ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) Fn ( ℂ × ℂ )
4 simpll ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ 𝑧 = ( 𝑥 + 𝑦 ) ) → 𝑥 ∈ ℂ )
5 simplr ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ 𝑧 = ( 𝑥 + 𝑦 ) ) → 𝑦 ∈ ℂ )
6 addcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
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 ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ