Theorem aannenlem3

Description: The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014)

	Ref	Expression
Hypothesis	aannenlem.a	$$⊢H=\left(a\in {\mathbb{N}}_0⟼\left\{b\in ℂ|\exists c\in \left\{d\in \mathrm{Poly}\left(\mathbb{Z}\right)|\left(d\ne 0_{𝑝}\wedge \mathrm{deg}\left(d\right)\le a\wedge \forall e\in {\mathbb{N}}_0\left|\mathrm{coeff}\left(d\right)\left(e\right)\right|\le a\right)\right\}c\left(b\right)=0\right\}\right)$$
Assertion	aannenlem3	$$⊢𝔸\approx \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		aannenlem.a	$$⊢H=\left(a\in {\mathbb{N}}_0⟼\left\{b\in ℂ|\exists c\in \left\{d\in \mathrm{Poly}\left(\mathbb{Z}\right)|\left(d\ne 0_{𝑝}\wedge \mathrm{deg}\left(d\right)\le a\wedge \forall e\in {\mathbb{N}}_0\left|\mathrm{coeff}\left(d\right)\left(e\right)\right|\le a\right)\right\}c\left(b\right)=0\right\}\right)$$
2	1	aannenlem2	$$⊢𝔸=\bigcup \mathrm{ran}H$$
3		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
4		nn0ennn	$$⊢{\mathbb{N}}_0\approx \mathbb{N}$$
5		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
6	4 5	entri	$$⊢{\mathbb{N}}_0\approx \mathrm{\omega }$$
7	6	ensymi	$$⊢\mathrm{\omega }\approx {\mathbb{N}}_0$$
8		isnumi	$$⊢\left(\mathrm{\omega }\in \mathrm{On}\wedge \mathrm{\omega }\approx {\mathbb{N}}_0\right)\to {\mathbb{N}}_0\in \mathrm{dom}\mathrm{card}$$
9	3 7 8	mp2an	$$⊢{\mathbb{N}}_0\in \mathrm{dom}\mathrm{card}$$
10		cnex	$$⊢ℂ\in \mathrm{V}$$
11	10	rabex	$$⊢\left\{b\in ℂ|\exists c\in \left\{d\in \mathrm{Poly}\left(\mathbb{Z}\right)|\left(d\ne 0_{𝑝}\wedge \mathrm{deg}\left(d\right)\le a\wedge \forall e\in {\mathbb{N}}_0\left|\mathrm{coeff}\left(d\right)\left(e\right)\right|\le a\right)\right\}c\left(b\right)=0\right\}\in \mathrm{V}$$
12	11 1	fnmpti	$$⊢HFn{\mathbb{N}}_0$$
13		dffn4	$$⊢HFn{\mathbb{N}}_0\leftrightarrow H:{\mathbb{N}}_0\underset{onto}{⟶}\mathrm{ran}H$$
14	12 13	mpbi	$$⊢H:{\mathbb{N}}_0\underset{onto}{⟶}\mathrm{ran}H$$
15		fodomnum	$$⊢{\mathbb{N}}_0\in \mathrm{dom}\mathrm{card}\to \left(H:{\mathbb{N}}_0\underset{onto}{⟶}\mathrm{ran}H\to \mathrm{ran}H\preccurlyeq {\mathbb{N}}_0\right)$$
16	9 14 15	mp2	$$⊢\mathrm{ran}H\preccurlyeq {\mathbb{N}}_0$$
17		domentr	$$⊢\left(\mathrm{ran}H\preccurlyeq {\mathbb{N}}_0\wedge {\mathbb{N}}_0\approx \mathrm{\omega }\right)\to \mathrm{ran}H\preccurlyeq \mathrm{\omega }$$
18	16 6 17	mp2an	$$⊢\mathrm{ran}H\preccurlyeq \mathrm{\omega }$$
19		fvelrnb	$$⊢HFn{\mathbb{N}}_0\to \left(f\in \mathrm{ran}H\leftrightarrow \exists g\in {\mathbb{N}}_{0}H\left(g\right)=f\right)$$
20	12 19	ax-mp	$$⊢f\in \mathrm{ran}H\leftrightarrow \exists g\in {\mathbb{N}}_{0}H\left(g\right)=f$$
21	1	aannenlem1	$$⊢g\in {\mathbb{N}}_0\to H\left(g\right)\in \mathrm{Fin}$$
22		eleq1	$$⊢H\left(g\right)=f\to \left(H\left(g\right)\in \mathrm{Fin}\leftrightarrow f\in \mathrm{Fin}\right)$$
23	21 22	syl5ibcom	$$⊢g\in {\mathbb{N}}_0\to \left(H\left(g\right)=f\to f\in \mathrm{Fin}\right)$$
24	23	rexlimiv	$$⊢\exists g\in {\mathbb{N}}_{0}H\left(g\right)=f\to f\in \mathrm{Fin}$$
25	20 24	sylbi	$$⊢f\in \mathrm{ran}H\to f\in \mathrm{Fin}$$
26	25	ssriv	$$⊢\mathrm{ran}H\subseteq \mathrm{Fin}$$
27		aasscn	$$⊢𝔸\subseteq ℂ$$
28	2 27	eqsstrri	$$⊢\bigcup \mathrm{ran}H\subseteq ℂ$$
29		soss	$$⊢\bigcup \mathrm{ran}H\subseteq ℂ\to \left(f\mathrm{Or}ℂ\to f\mathrm{Or}\bigcup \mathrm{ran}H\right)$$
30	28 29	ax-mp	$$⊢f\mathrm{Or}ℂ\to f\mathrm{Or}\bigcup \mathrm{ran}H$$
31		iunfictbso	$$⊢\left(\mathrm{ran}H\preccurlyeq \mathrm{\omega }\wedge \mathrm{ran}H\subseteq \mathrm{Fin}\wedge f\mathrm{Or}\bigcup \mathrm{ran}H\right)\to \bigcup \mathrm{ran}H\preccurlyeq \mathrm{\omega }$$
32	18 26 30 31	mp3an12i	$$⊢f\mathrm{Or}ℂ\to \bigcup \mathrm{ran}H\preccurlyeq \mathrm{\omega }$$
33	2 32	eqbrtrid	$$⊢f\mathrm{Or}ℂ\to 𝔸\preccurlyeq \mathrm{\omega }$$
34		cnso	$$⊢\exists ff\mathrm{Or}ℂ$$
35	33 34	exlimiiv	$$⊢𝔸\preccurlyeq \mathrm{\omega }$$
36	5	ensymi	$$⊢\mathrm{\omega }\approx \mathbb{N}$$
37		domentr	$$⊢\left(𝔸\preccurlyeq \mathrm{\omega }\wedge \mathrm{\omega }\approx \mathbb{N}\right)\to 𝔸\preccurlyeq \mathbb{N}$$
38	35 36 37	mp2an	$$⊢𝔸\preccurlyeq \mathbb{N}$$
39	10 27	ssexi	$$⊢𝔸\in \mathrm{V}$$
40		nnssq	$$⊢\mathbb{N}\subseteq \mathbb{Q}$$
41		qssaa	$$⊢\mathbb{Q}\subseteq 𝔸$$
42	40 41	sstri	$$⊢\mathbb{N}\subseteq 𝔸$$
43		ssdomg	$$⊢𝔸\in \mathrm{V}\to \left(\mathbb{N}\subseteq 𝔸\to \mathbb{N}\preccurlyeq 𝔸\right)$$
44	39 42 43	mp2	$$⊢\mathbb{N}\preccurlyeq 𝔸$$
45		sbth	$$⊢\left(𝔸\preccurlyeq \mathbb{N}\wedge \mathbb{N}\preccurlyeq 𝔸\right)\to 𝔸\approx \mathbb{N}$$
46	38 44 45	mp2an	$$⊢𝔸\approx \mathbb{N}$$