Theorem bj-ccinftydisj

Description: The circle at infinity is disjoint from the set of complex numbers. (Contributed by BJ, 22-Jun-2019)

	Ref	Expression
Assertion	bj-ccinftydisj	$$⊢ℂ\cap {ℂ}_{\infty }=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		bj-inftyexpidisj	$$⊢\neg inftyexpi\left(y\right)\in ℂ$$
2	1	nex	$$⊢\neg \exists yinftyexpi\left(y\right)\in ℂ$$
3		elin	$$⊢x\in \left(ℂ\cap {ℂ}_{\infty }\right)\leftrightarrow \left(x\in ℂ\wedge x\in {ℂ}_{\infty }\right)$$
4		df-bj-inftyexpi	$$⊢inftyexpi=\left(z\in \left(-\mathrm{\pi },\mathrm{\pi }\right]⟼⟨z,ℂ⟩\right)$$
5	4	funmpt2	$$⊢\mathrm{Fun}inftyexpi$$
6		elrnrexdm	$$⊢\mathrm{Fun}inftyexpi\to \left(x\in \mathrm{ran}inftyexpi\to \exists y\in \mathrm{dom}inftyexpix=inftyexpi\left(y\right)\right)$$
7	5 6	ax-mp	$$⊢x\in \mathrm{ran}inftyexpi\to \exists y\in \mathrm{dom}inftyexpix=inftyexpi\left(y\right)$$
8		rexex	$$⊢\exists y\in \mathrm{dom}inftyexpix=inftyexpi\left(y\right)\to \exists yx=inftyexpi\left(y\right)$$
9	7 8	syl	$$⊢x\in \mathrm{ran}inftyexpi\to \exists yx=inftyexpi\left(y\right)$$
10		df-bj-ccinfty	$$⊢{ℂ}_{\infty }=\mathrm{ran}inftyexpi$$
11	9 10	eleq2s	$$⊢x\in {ℂ}_{\infty }\to \exists yx=inftyexpi\left(y\right)$$
12	11	anim2i	$$⊢\left(x\in ℂ\wedge x\in {ℂ}_{\infty }\right)\to \left(x\in ℂ\wedge \exists yx=inftyexpi\left(y\right)\right)$$
13	3 12	sylbi	$$⊢x\in \left(ℂ\cap {ℂ}_{\infty }\right)\to \left(x\in ℂ\wedge \exists yx=inftyexpi\left(y\right)\right)$$
14		ancom	$$⊢\left(x\in ℂ\wedge \exists yx=inftyexpi\left(y\right)\right)\leftrightarrow \left(\exists yx=inftyexpi\left(y\right)\wedge x\in ℂ\right)$$
15		exancom	$$⊢\exists y\left(x\in ℂ\wedge x=inftyexpi\left(y\right)\right)\leftrightarrow \exists y\left(x=inftyexpi\left(y\right)\wedge x\in ℂ\right)$$
16		19.41v	$$⊢\exists y\left(x=inftyexpi\left(y\right)\wedge x\in ℂ\right)\leftrightarrow \left(\exists yx=inftyexpi\left(y\right)\wedge x\in ℂ\right)$$
17	15 16	bitri	$$⊢\exists y\left(x\in ℂ\wedge x=inftyexpi\left(y\right)\right)\leftrightarrow \left(\exists yx=inftyexpi\left(y\right)\wedge x\in ℂ\right)$$
18	14 17	sylbb2	$$⊢\left(x\in ℂ\wedge \exists yx=inftyexpi\left(y\right)\right)\to \exists y\left(x\in ℂ\wedge x=inftyexpi\left(y\right)\right)$$
19	13 18	syl	$$⊢x\in \left(ℂ\cap {ℂ}_{\infty }\right)\to \exists y\left(x\in ℂ\wedge x=inftyexpi\left(y\right)\right)$$
20		eleq1	$$⊢x=inftyexpi\left(y\right)\to \left(x\in ℂ\leftrightarrow inftyexpi\left(y\right)\in ℂ\right)$$
21	20	biimpac	$$⊢\left(x\in ℂ\wedge x=inftyexpi\left(y\right)\right)\to inftyexpi\left(y\right)\in ℂ$$
22	21	eximi	$$⊢\exists y\left(x\in ℂ\wedge x=inftyexpi\left(y\right)\right)\to \exists yinftyexpi\left(y\right)\in ℂ$$
23	19 22	syl	$$⊢x\in \left(ℂ\cap {ℂ}_{\infty }\right)\to \exists yinftyexpi\left(y\right)\in ℂ$$
24	2 23	mto	$$⊢\neg x\in \left(ℂ\cap {ℂ}_{\infty }\right)$$
25	24	nel0	$$⊢ℂ\cap {ℂ}_{\infty }=\varnothing$$