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 e. CC , y e. CC |-> ( x + y ) ) : ( CC X. CC ) --> CC

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( x e. CC , y e. CC |-> ( x + y ) ) = ( x e. CC , y e. CC |-> ( x + y ) )
2 ovex 
 |-  ( x + y ) e. _V
3 1 2 fnmpoi 
 |-  ( x e. CC , y e. CC |-> ( x + y ) ) Fn ( CC X. CC )
4 simpll 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ z = ( x + y ) ) -> x e. CC )
5 simplr 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ z = ( x + y ) ) -> y e. CC )
6 addcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
7 eleq1a 
 |-  ( ( x + y ) e. CC -> ( z = ( x + y ) -> z e. CC ) )
8 6 7 syl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( z = ( x + y ) -> z e. CC ) )
9 8 imp 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ z = ( x + y ) ) -> z e. CC )
10 4 5 9 3jca 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ z = ( x + y ) ) -> ( x e. CC /\ y e. CC /\ z e. CC ) )
11 10 ssoprab2i 
 |-  { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ z = ( x + y ) ) } C_ { <. <. x , y >. , z >. | ( x e. CC /\ y e. CC /\ z e. CC ) }
12 df-mpo 
 |-  ( x e. CC , y e. CC |-> ( x + y ) ) = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ z = ( x + y ) ) }
13 dfxp3 
 |-  ( ( CC X. CC ) X. CC ) = { <. <. x , y >. , z >. | ( x e. CC /\ y e. CC /\ z e. CC ) }
14 11 12 13 3sstr4i 
 |-  ( x e. CC , y e. CC |-> ( x + y ) ) C_ ( ( CC X. CC ) X. CC )
15 dff2 
 |-  ( ( x e. CC , y e. CC |-> ( x + y ) ) : ( CC X. CC ) --> CC <-> ( ( x e. CC , y e. CC |-> ( x + y ) ) Fn ( CC X. CC ) /\ ( x e. CC , y e. CC |-> ( x + y ) ) C_ ( ( CC X. CC ) X. CC ) ) )
16 3 14 15 mpbir2an 
 |-  ( x e. CC , y e. CC |-> ( x + y ) ) : ( CC X. CC ) --> CC