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 31725
 Description: The circle at infinity is disjoint from the set of complex numbers. (Contributed by BJ, 22-Jun-2019.)
Assertion
Ref Expression
bj-ccinftydisj CCinfty

Proof of Theorem bj-ccinftydisj
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bj-inftyexpidisj 31722 . . . 4 inftyexpi
21nex 1686 . . 3 inftyexpi
3 elin 3608 . . . . . 6 CCinfty CCinfty
4 df-bj-inftyexpi 31719 . . . . . . . . . . 11 inftyexpi
54funmpt2 5626 . . . . . . . . . 10 inftyexpi
6 elrnrexdm 6041 . . . . . . . . . 10 inftyexpi inftyexpi inftyexpi inftyexpi
75, 6ax-mp 5 . . . . . . . . 9 inftyexpi inftyexpi inftyexpi
8 rexex 2843 . . . . . . . . 9 inftyexpi inftyexpi inftyexpi
97, 8syl 17 . . . . . . . 8 inftyexpi inftyexpi
10 df-bj-ccinfty 31724 . . . . . . . 8 CCinfty inftyexpi
119, 10eleq2s 2567 . . . . . . 7 CCinfty inftyexpi
1211anim2i 579 . . . . . 6 CCinfty inftyexpi
133, 12sylbi 200 . . . . 5 CCinfty inftyexpi
14 ancom 457 . . . . . 6 inftyexpi inftyexpi
15 exancom 1730 . . . . . . 7 inftyexpi inftyexpi
16 19.41v 1838 . . . . . . 7 inftyexpi inftyexpi
1715, 16bitri 257 . . . . . 6 inftyexpi inftyexpi
1814, 17sylbb2 221 . . . . 5 inftyexpi inftyexpi
1913, 18syl 17 . . . 4 CCinfty inftyexpi
20 eleq1 2537 . . . . . 6 inftyexpi inftyexpi
2120biimpac 494 . . . . 5 inftyexpi inftyexpi
2221eximi 1715 . . . 4 inftyexpi inftyexpi
2319, 22syl 17 . . 3 CCinfty inftyexpi
242, 23mto 181 . 2 CCinfty
2524bj-nel0 31611 1 CCinfty
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 376   wceq 1452  wex 1671   wcel 1904  wrex 2757   cin 3389  c0 3722  cop 3965   cdm 4839   crn 4840   wfun 5583  cfv 5589  (class class class)co 6308  cc 9555  cneg 9881  cioc 11661  cpi 14196  inftyexpi cinftyexpi 31718  CCinftycccinfty 31723 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-reg 8125  ax-cnex 9613 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-iota 5553  df-fun 5591  df-fn 5592  df-fv 5597  df-c 9563  df-bj-inftyexpi 31719  df-bj-ccinfty 31724 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator