Theorem bj-minftyccb

Description: The class minfty is an extended complex number. (Contributed by BJ, 27-Jun-2019)

	Ref	Expression
Assertion	bj-minftyccb	|- minfty e. CCbar

Proof

Step	Hyp	Ref	Expression
1		bj-ccinftyssccbar	|- CCinfty C_ CCbar
2		df-bj-inftyexpi	|- inftyexpi = ( x e. ( -u _pi (,] _pi ) |-> <. x , CC >. )
3	2	funmpt2	|- Fun inftyexpi
4		pire	|- _pi e. RR
5	4	renegcli	|- -u _pi e. RR
6	5	rexri	|- -u _pi e. RR*
7	4	rexri	|- _pi e. RR*
8		pipos	|- 0 < _pi
9		0re	|- 0 e. RR
10	9 4	ltnegi	|- ( 0 < _pi <-> -u _pi < -u 0 )
11	8 10	mpbi	|- -u _pi < -u 0
12		neg0	|- -u 0 = 0
13	11 12	breqtri	|- -u _pi < 0
14	5 9 4	lttri	|- ( ( -u _pi < 0 /\ 0 < _pi ) -> -u _pi < _pi )
15	13 8 14	mp2an	|- -u _pi < _pi
16		ubioc1	|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ -u _pi < _pi ) -> _pi e. ( -u _pi (,] _pi ) )
17	6 7 15 16	mp3an	|- _pi e. ( -u _pi (,] _pi )
18		opex	|- <. x , CC >. e. _V
19	18 2	dmmpti	|- dom inftyexpi = ( -u _pi (,] _pi )
20	17 19	eleqtrri	|- _pi e. dom inftyexpi
21		fvelrn	|- ( ( Fun inftyexpi /\ _pi e. dom inftyexpi ) -> ( inftyexpi ` _pi ) e. ran inftyexpi )
22	3 20 21	mp2an	|- ( inftyexpi ` _pi ) e. ran inftyexpi
23		df-bj-minfty	|- minfty = ( inftyexpi ` _pi )
24		df-bj-ccinfty	|- CCinfty = ran inftyexpi
25	22 23 24	3eltr4i	|- minfty e. CCinfty
26	1 25	sselii	|- minfty e. CCbar