Metamath Proof Explorer

Theorem bj-ccinftydisj

Description: The circle at infinity is disjoint from the set of complex numbers. (Contributed by BJ, 22-Jun-2019)

Ref Expression
Assertion bj-ccinftydisj 
|- ( CC i^i CCinfty ) = (/)

Proof

Step Hyp Ref Expression
1 bj-inftyexpidisj 
 |-  -. ( inftyexpi ` y ) e. CC
2 1 nex 
 |-  -. E. y ( inftyexpi ` y ) e. CC
3 elin 
 |-  ( x e. ( CC i^i CCinfty ) <-> ( x e. CC /\ x e. CCinfty ) )
4 df-bj-inftyexpi 
 |-  inftyexpi = ( z e. ( -u _pi (,] _pi ) |-> <. z , CC >. )
5 4 funmpt2 
 |-  Fun inftyexpi
6 elrnrexdm 
 |-  ( Fun inftyexpi -> ( x e. ran inftyexpi -> E. y e. dom inftyexpi x = ( inftyexpi ` y ) ) )
7 5 6 ax-mp 
 |-  ( x e. ran inftyexpi -> E. y e. dom inftyexpi x = ( inftyexpi ` y ) )
8 rexex 
 |-  ( E. y e. dom inftyexpi x = ( inftyexpi ` y ) -> E. y x = ( inftyexpi ` y ) )
9 7 8 syl 
 |-  ( x e. ran inftyexpi -> E. y x = ( inftyexpi ` y ) )
10 df-bj-ccinfty 
 |-  CCinfty = ran inftyexpi
11 9 10 eleq2s 
 |-  ( x e. CCinfty -> E. y x = ( inftyexpi ` y ) )
12 11 anim2i 
 |-  ( ( x e. CC /\ x e. CCinfty ) -> ( x e. CC /\ E. y x = ( inftyexpi ` y ) ) )
13 3 12 sylbi 
 |-  ( x e. ( CC i^i CCinfty ) -> ( x e. CC /\ E. y x = ( inftyexpi ` y ) ) )
14 ancom 
 |-  ( ( x e. CC /\ E. y x = ( inftyexpi ` y ) ) <-> ( E. y x = ( inftyexpi ` y ) /\ x e. CC ) )
15 exancom 
 |-  ( E. y ( x e. CC /\ x = ( inftyexpi ` y ) ) <-> E. y ( x = ( inftyexpi ` y ) /\ x e. CC ) )
16 19.41v 
 |-  ( E. y ( x = ( inftyexpi ` y ) /\ x e. CC ) <-> ( E. y x = ( inftyexpi ` y ) /\ x e. CC ) )
17 15 16 bitri 
 |-  ( E. y ( x e. CC /\ x = ( inftyexpi ` y ) ) <-> ( E. y x = ( inftyexpi ` y ) /\ x e. CC ) )
18 14 17 sylbb2 
 |-  ( ( x e. CC /\ E. y x = ( inftyexpi ` y ) ) -> E. y ( x e. CC /\ x = ( inftyexpi ` y ) ) )
19 13 18 syl 
 |-  ( x e. ( CC i^i CCinfty ) -> E. y ( x e. CC /\ x = ( inftyexpi ` y ) ) )
20 eleq1 
 |-  ( x = ( inftyexpi ` y ) -> ( x e. CC <-> ( inftyexpi ` y ) e. CC ) )
21 20 biimpac 
 |-  ( ( x e. CC /\ x = ( inftyexpi ` y ) ) -> ( inftyexpi ` y ) e. CC )
22 21 eximi 
 |-  ( E. y ( x e. CC /\ x = ( inftyexpi ` y ) ) -> E. y ( inftyexpi ` y ) e. CC )
23 19 22 syl 
 |-  ( x e. ( CC i^i CCinfty ) -> E. y ( inftyexpi ` y ) e. CC )
24 2 23 mto 
 |-  -. x e. ( CC i^i CCinfty )
25 24 nel0 
 |-  ( CC i^i CCinfty ) = (/)