Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-ccinftydisj Structured version   Visualization version   Unicode version

Theorem bj-ccinftydisj 31655
Description: The circle at infinity is disjoint from the set of complex numbers. (Contributed by BJ, 22-Jun-2019.)
Assertion
Ref Expression
bj-ccinftydisj  |-  ( CC 
i^i CCinfty )  =  (/)

Proof of Theorem bj-ccinftydisj
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bj-inftyexpidisj 31652 . . . 4  |-  -.  (inftyexpi  `  y )  e.  CC
21nex 1678 . . 3  |-  -.  E. y (inftyexpi  `  y )  e.  CC
3 elin 3617 . . . . . 6  |-  ( x  e.  ( CC  i^i CCinfty )  <-> 
( x  e.  CC  /\  x  e. CCinfty ) )
4 df-bj-inftyexpi 31649 . . . . . . . . . . 11  |- inftyexpi  =  ( z  e.  ( -u pi (,] pi )  |->  <.
z ,  CC >. )
54funmpt2 5619 . . . . . . . . . 10  |-  Fun inftyexpi
6 elrnrexdm 6026 . . . . . . . . . 10  |-  ( Fun inftyexpi  -> 
( x  e.  ran inftyexpi  ->  E. y  e.  dom inftyexpi  x  =  (inftyexpi  `  y ) ) )
75, 6ax-mp 5 . . . . . . . . 9  |-  ( x  e.  ran inftyexpi  ->  E. y  e.  dom inftyexpi  x  =  (inftyexpi  `  y ) )
8 rexex 2844 . . . . . . . . 9  |-  ( E. y  e.  dom inftyexpi  x  =  (inftyexpi  `  y )  ->  E. y  x  =  (inftyexpi  `
 y ) )
97, 8syl 17 . . . . . . . 8  |-  ( x  e.  ran inftyexpi  ->  E. y  x  =  (inftyexpi  `  y
) )
10 df-bj-ccinfty 31654 . . . . . . . 8  |- CCinfty  =  ran inftyexpi
119, 10eleq2s 2547 . . . . . . 7  |-  ( x  e. CCinfty  ->  E. y  x  =  (inftyexpi  `  y ) )
1211anim2i 573 . . . . . 6  |-  ( ( x  e.  CC  /\  x  e. CCinfty )  ->  (
x  e.  CC  /\  E. y  x  =  (inftyexpi  `  y ) ) )
133, 12sylbi 199 . . . . 5  |-  ( x  e.  ( CC  i^i CCinfty )  ->  ( x  e.  CC  /\  E. y  x  =  (inftyexpi  `  y
) ) )
14 ancom 452 . . . . . 6  |-  ( ( x  e.  CC  /\  E. y  x  =  (inftyexpi  `  y ) )  <->  ( E. y  x  =  (inftyexpi  `  y )  /\  x  e.  CC ) )
15 exancom 1722 . . . . . . 7  |-  ( E. y ( x  e.  CC  /\  x  =  (inftyexpi  `  y ) )  <->  E. y ( x  =  (inftyexpi  `  y )  /\  x  e.  CC )
)
16 19.41v 1830 . . . . . . 7  |-  ( E. y ( x  =  (inftyexpi  `  y )  /\  x  e.  CC )  <->  ( E. y  x  =  (inftyexpi  `  y )  /\  x  e.  CC )
)
1715, 16bitri 253 . . . . . 6  |-  ( E. y ( x  e.  CC  /\  x  =  (inftyexpi  `  y ) )  <-> 
( E. y  x  =  (inftyexpi  `  y )  /\  x  e.  CC ) )
1814, 17sylbb2 31128 . . . . 5  |-  ( ( x  e.  CC  /\  E. y  x  =  (inftyexpi  `  y ) )  ->  E. y ( x  e.  CC  /\  x  =  (inftyexpi  `  y ) ) )
1913, 18syl 17 . . . 4  |-  ( x  e.  ( CC  i^i CCinfty )  ->  E. y ( x  e.  CC  /\  x  =  (inftyexpi  `  y ) ) )
20 eleq1 2517 . . . . . 6  |-  ( x  =  (inftyexpi  `  y )  ->  ( x  e.  CC  <->  (inftyexpi  `  y )  e.  CC ) )
2120biimpac 489 . . . . 5  |-  ( ( x  e.  CC  /\  x  =  (inftyexpi  `  y
) )  ->  (inftyexpi  `  y )  e.  CC )
2221eximi 1707 . . . 4  |-  ( E. y ( x  e.  CC  /\  x  =  (inftyexpi  `  y ) )  ->  E. y (inftyexpi  `  y
)  e.  CC )
2319, 22syl 17 . . 3  |-  ( x  e.  ( CC  i^i CCinfty )  ->  E. y (inftyexpi  `  y
)  e.  CC )
242, 23mto 180 . 2  |-  -.  x  e.  ( CC  i^i CCinfty )
2524bj-nel0 31541 1  |-  ( CC 
i^i CCinfty )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1444   E.wex 1663    e. wcel 1887   E.wrex 2738    i^i cin 3403   (/)c0 3731   <.cop 3974   dom cdm 4834   ran crn 4835   Fun wfun 5576   ` cfv 5582  (class class class)co 6290   CCcc 9537   -ucneg 9861   (,]cioc 11636   picpi 14119  inftyexpi cinftyexpi 31648  CCinftycccinfty 31653
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-reg 8107  ax-cnex 9595
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-iota 5546  df-fun 5584  df-fn 5585  df-fv 5590  df-c 9545  df-bj-inftyexpi 31649  df-bj-ccinfty 31654
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator