Metamath Proof Explorer

Theorem cnso

Description: The complex numbers can be linearly ordered. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion cnso 
|- E. x x Or CC

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 eqid 
 |-  { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } = { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) }
3 f1oiso 
 |-  ( ( a : RR -1-1-onto-> CC /\ { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } = { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } ) -> a Isom < , { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } ( RR , CC ) )
4 2 3 mpan2 
 |-  ( a : RR -1-1-onto-> CC -> a Isom < , { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } ( RR , CC ) )
5 isoso 
 |-  ( a Isom < , { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } ( RR , CC ) -> ( < Or RR <-> { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } Or CC ) )
6 soinxp 
 |-  ( { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } Or CC <-> ( { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } i^i ( CC X. CC ) ) Or CC )
7 5 6 bitrdi 
 |-  ( a Isom < , { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } ( RR , CC ) -> ( < Or RR <-> ( { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } i^i ( CC X. CC ) ) Or CC ) )
8 4 7 syl 
 |-  ( a : RR -1-1-onto-> CC -> ( < Or RR <-> ( { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } i^i ( CC X. CC ) ) Or CC ) )
9 1 8 mpbii 
 |-  ( a : RR -1-1-onto-> CC -> ( { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } i^i ( CC X. CC ) ) Or CC )
10 cnex 
 |-  CC e. _V
11 10 10 xpex 
 |-  ( CC X. CC ) e. _V
12 11 inex2 
 |-  ( { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } i^i ( CC X. CC ) ) e. _V
13 soeq1 
 |-  ( x = ( { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } i^i ( CC X. CC ) ) -> ( x Or CC <-> ( { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } i^i ( CC X. CC ) ) Or CC ) )
14 12 13 spcev 
 |-  ( ( { <. b , c >. | E. d e. RR E. e e. RR ( ( b = ( a ` d ) /\ c = ( a ` e ) ) /\ d < e ) } i^i ( CC X. CC ) ) Or CC -> E. x x Or CC )
15 9 14 syl 
 |-  ( a : RR -1-1-onto-> CC -> E. x x Or CC )
16 rpnnen 
 |-  RR ~~ ~P NN
17 cpnnen 
 |-  CC ~~ ~P NN
18 16 17 entr4i 
 |-  RR ~~ CC
19 bren 
 |-  ( RR ~~ CC <-> E. a a : RR -1-1-onto-> CC )
20 18 19 mpbi 
 |-  E. a a : RR -1-1-onto-> CC
21 15 20 exlimiiv 
 |-  E. x x Or CC