Metamath Proof Explorer

Theorem bj-elccinfty

Description: A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019)

Ref Expression
Assertion bj-elccinfty 
|- ( A e. ( -u _pi (,] _pi ) -> ( inftyexpi ` A ) e. CCinfty )

Proof

Step Hyp Ref Expression
1 df-bj-inftyexpi 
 |-  inftyexpi = ( x e. ( -u _pi (,] _pi ) |-> <. x , CC >. )
2 1 funmpt2 
 |-  Fun inftyexpi
3 2 jctl 
 |-  ( A e. dom inftyexpi -> ( Fun inftyexpi /\ A e. dom inftyexpi ) )
4 opex 
 |-  <. x , CC >. e. _V
5 4 1 dmmpti 
 |-  dom inftyexpi = ( -u _pi (,] _pi )
6 5 eqcomi 
 |-  ( -u _pi (,] _pi ) = dom inftyexpi
7 3 6 eleq2s 
 |-  ( A e. ( -u _pi (,] _pi ) -> ( Fun inftyexpi /\ A e. dom inftyexpi ) )
8 fvelrn 
 |-  ( ( Fun inftyexpi /\ A e. dom inftyexpi ) -> ( inftyexpi ` A ) e. ran inftyexpi )
9 df-bj-ccinfty 
 |-  CCinfty = ran inftyexpi
10 9 eqcomi 
 |-  ran inftyexpi = CCinfty
11 10 eleq2i 
 |-  ( ( inftyexpi ` A ) e. ran inftyexpi <-> ( inftyexpi ` A ) e. CCinfty )
12 11 biimpi 
 |-  ( ( inftyexpi ` A ) e. ran inftyexpi -> ( inftyexpi ` A ) e. CCinfty )
13 7 8 12 3syl 
 |-  ( A e. ( -u _pi (,] _pi ) -> ( inftyexpi ` A ) e. CCinfty )