Theorem bj-minftyccb

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

	Ref	Expression
Assertion	bj-minftyccb	⊢ -∞ ∈ ℂ̅

Proof

Step	Hyp	Ref	Expression
1		bj-ccinftyssccbar	⊢ ℂ∞ ⊆ ℂ̅
2		df-bj-inftyexpi	⊢ +∞ei = ( 𝑥 ∈ ( - π (,] π ) ↦ ⟨ 𝑥 , ℂ ⟩ )
3	2	funmpt2	⊢ Fun +∞ei
4		pire	⊢ π ∈ ℝ
5	4	renegcli	⊢ - π ∈ ℝ
6	5	rexri	⊢ - π ∈ ℝ*
7	4	rexri	⊢ π ∈ ℝ*
8		pipos	⊢ 0 < π
9		0re	⊢ 0 ∈ ℝ
10	9 4	ltnegi	⊢ ( 0 < π ↔ - π < - 0 )
11	8 10	mpbi	⊢ - π < - 0
12		neg0	⊢ - 0 = 0
13	11 12	breqtri	⊢ - π < 0
14	5 9 4	lttri	⊢ ( ( - π < 0 ∧ 0 < π ) → - π < π )
15	13 8 14	mp2an	⊢ - π < π
16		ubioc1	⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ - π < π ) → π ∈ ( - π (,] π ) )
17	6 7 15 16	mp3an	⊢ π ∈ ( - π (,] π )
18		opex	⊢ ⟨ 𝑥 , ℂ ⟩ ∈ V
19	18 2	dmmpti	⊢ dom +∞ei = ( - π (,] π )
20	17 19	eleqtrri	⊢ π ∈ dom +∞ei
21		fvelrn	⊢ ( ( Fun +∞ei ∧ π ∈ dom +∞ei ) → ( +∞ei ‘ π ) ∈ ran +∞ei )
22	3 20 21	mp2an	⊢ ( +∞ei ‘ π ) ∈ ran +∞ei
23		df-bj-minfty	⊢ -∞ = ( +∞ei ‘ π )
24		df-bj-ccinfty	⊢ ℂ∞ = ran +∞ei
25	22 23 24	3eltr4i	⊢ -∞ ∈ ℂ∞
26	1 25	sselii	⊢ -∞ ∈ ℂ̅