Metamath Proof Explorer

Theorem cnexALT

Description: The set of complex numbers exists. This theorem shows that ax-cnex is redundant if we assume ax-rep . See also ax-cnex . (Contributed by NM, 30-Jul-2004) (Revised by Mario Carneiro, 16-Jun-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnexALT 
|- CC e. _V

Proof

Step Hyp Ref Expression
1 reexALT 
 |-  RR e. _V
2 1 1 xpex 
 |-  ( RR X. RR ) e. _V
3 eqid 
 |-  ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) ) = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )
4 3 cnref1o 
 |-  ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) ) : ( RR X. RR ) -1-1-onto-> CC
5 f1ofo 
 |-  ( ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) ) : ( RR X. RR ) -1-1-onto-> CC -> ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) ) : ( RR X. RR ) -onto-> CC )
6 4 5 ax-mp 
 |-  ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) ) : ( RR X. RR ) -onto-> CC
7 focdmex 
 |-  ( ( RR X. RR ) e. _V -> ( ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) ) : ( RR X. RR ) -onto-> CC -> CC e. _V ) )
8 2 6 7 mp2 
 |-  CC e. _V