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	⊢ ( ℂ ∩ ℂ∞ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		bj-inftyexpidisj	⊢ ¬ ( +∞ei ‘ 𝑦 ) ∈ ℂ
2	1	nex	⊢ ¬ ∃ 𝑦 ( +∞ei ‘ 𝑦 ) ∈ ℂ
3		elin	⊢ ( 𝑥 ∈ ( ℂ ∩ ℂ∞ ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 ∈ ℂ∞ ) )
4		df-bj-inftyexpi	⊢ +∞ei = ( 𝑧 ∈ ( - π (,] π ) ↦ ⟨ 𝑧 , ℂ ⟩ )
5	4	funmpt2	⊢ Fun +∞ei
6		elrnrexdm	⊢ ( Fun +∞ei → ( 𝑥 ∈ ran +∞ei → ∃ 𝑦 ∈ dom +∞ei 𝑥 = ( +∞ei ‘ 𝑦 ) ) )
7	5 6	ax-mp	⊢ ( 𝑥 ∈ ran +∞ei → ∃ 𝑦 ∈ dom +∞ei 𝑥 = ( +∞ei ‘ 𝑦 ) )
8		rexex	⊢ ( ∃ 𝑦 ∈ dom +∞ei 𝑥 = ( +∞ei ‘ 𝑦 ) → ∃ 𝑦 𝑥 = ( +∞ei ‘ 𝑦 ) )
9	7 8	syl	⊢ ( 𝑥 ∈ ran +∞ei → ∃ 𝑦 𝑥 = ( +∞ei ‘ 𝑦 ) )
10		df-bj-ccinfty	⊢ ℂ∞ = ran +∞ei
11	9 10	eleq2s	⊢ ( 𝑥 ∈ ℂ∞ → ∃ 𝑦 𝑥 = ( +∞ei ‘ 𝑦 ) )
12	11	anim2i	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ∈ ℂ∞ ) → ( 𝑥 ∈ ℂ ∧ ∃ 𝑦 𝑥 = ( +∞ei ‘ 𝑦 ) ) )
13	3 12	sylbi	⊢ ( 𝑥 ∈ ( ℂ ∩ ℂ∞ ) → ( 𝑥 ∈ ℂ ∧ ∃ 𝑦 𝑥 = ( +∞ei ‘ 𝑦 ) ) )
14		ancom	⊢ ( ( 𝑥 ∈ ℂ ∧ ∃ 𝑦 𝑥 = ( +∞ei ‘ 𝑦 ) ) ↔ ( ∃ 𝑦 𝑥 = ( +∞ei ‘ 𝑦 ) ∧ 𝑥 ∈ ℂ ) )
15		exancom	⊢ ( ∃ 𝑦 ( 𝑥 ∈ ℂ ∧ 𝑥 = ( +∞ei ‘ 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑥 = ( +∞ei ‘ 𝑦 ) ∧ 𝑥 ∈ ℂ ) )
16		19.41v	⊢ ( ∃ 𝑦 ( 𝑥 = ( +∞ei ‘ 𝑦 ) ∧ 𝑥 ∈ ℂ ) ↔ ( ∃ 𝑦 𝑥 = ( +∞ei ‘ 𝑦 ) ∧ 𝑥 ∈ ℂ ) )
17	15 16	bitri	⊢ ( ∃ 𝑦 ( 𝑥 ∈ ℂ ∧ 𝑥 = ( +∞ei ‘ 𝑦 ) ) ↔ ( ∃ 𝑦 𝑥 = ( +∞ei ‘ 𝑦 ) ∧ 𝑥 ∈ ℂ ) )
18	14 17	sylbb2	⊢ ( ( 𝑥 ∈ ℂ ∧ ∃ 𝑦 𝑥 = ( +∞ei ‘ 𝑦 ) ) → ∃ 𝑦 ( 𝑥 ∈ ℂ ∧ 𝑥 = ( +∞ei ‘ 𝑦 ) ) )
19	13 18	syl	⊢ ( 𝑥 ∈ ( ℂ ∩ ℂ∞ ) → ∃ 𝑦 ( 𝑥 ∈ ℂ ∧ 𝑥 = ( +∞ei ‘ 𝑦 ) ) )
20		eleq1	⊢ ( 𝑥 = ( +∞ei ‘ 𝑦 ) → ( 𝑥 ∈ ℂ ↔ ( +∞ei ‘ 𝑦 ) ∈ ℂ ) )
21	20	biimpac	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 = ( +∞ei ‘ 𝑦 ) ) → ( +∞ei ‘ 𝑦 ) ∈ ℂ )
22	21	eximi	⊢ ( ∃ 𝑦 ( 𝑥 ∈ ℂ ∧ 𝑥 = ( +∞ei ‘ 𝑦 ) ) → ∃ 𝑦 ( +∞ei ‘ 𝑦 ) ∈ ℂ )
23	19 22	syl	⊢ ( 𝑥 ∈ ( ℂ ∩ ℂ∞ ) → ∃ 𝑦 ( +∞ei ‘ 𝑦 ) ∈ ℂ )
24	2 23	mto	⊢ ¬ 𝑥 ∈ ( ℂ ∩ ℂ∞ )
25	24	nel0	⊢ ( ℂ ∩ ℂ∞ ) = ∅