Theorem aannenlem3

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

	Ref	Expression
Hypothesis	aannenlem.a	⊢ 𝐻 = ( 𝑎 ∈ ℕ0 ↦ { 𝑏 ∈ ℂ ∣ ∃ 𝑐 ∈ { 𝑑 ∈ ( Poly ‘ ℤ ) ∣ ( 𝑑 ≠ 0𝑝 ∧ ( deg ‘ 𝑑 ) ≤ 𝑎 ∧ ∀ 𝑒 ∈ ℕ0 ( abs ‘ ( ( coeff ‘ 𝑑 ) ‘ 𝑒 ) ) ≤ 𝑎 ) } ( 𝑐 ‘ 𝑏 ) = 0 } )
Assertion	aannenlem3	⊢ 𝔸 ≈ ℕ

Proof

Step	Hyp	Ref	Expression
1		aannenlem.a	⊢ 𝐻 = ( 𝑎 ∈ ℕ0 ↦ { 𝑏 ∈ ℂ ∣ ∃ 𝑐 ∈ { 𝑑 ∈ ( Poly ‘ ℤ ) ∣ ( 𝑑 ≠ 0𝑝 ∧ ( deg ‘ 𝑑 ) ≤ 𝑎 ∧ ∀ 𝑒 ∈ ℕ0 ( abs ‘ ( ( coeff ‘ 𝑑 ) ‘ 𝑒 ) ) ≤ 𝑎 ) } ( 𝑐 ‘ 𝑏 ) = 0 } )
2	1	aannenlem2	⊢ 𝔸 = ∪ ran 𝐻
3		omelon	⊢ ω ∈ On
4		nn0ennn	⊢ ℕ0 ≈ ℕ
5		nnenom	⊢ ℕ ≈ ω
6	4 5	entri	⊢ ℕ0 ≈ ω
7	6	ensymi	⊢ ω ≈ ℕ0
8		isnumi	⊢ ( ( ω ∈ On ∧ ω ≈ ℕ0 ) → ℕ0 ∈ dom card )
9	3 7 8	mp2an	⊢ ℕ0 ∈ dom card
10		cnex	⊢ ℂ ∈ V
11	10	rabex	⊢ { 𝑏 ∈ ℂ ∣ ∃ 𝑐 ∈ { 𝑑 ∈ ( Poly ‘ ℤ ) ∣ ( 𝑑 ≠ 0𝑝 ∧ ( deg ‘ 𝑑 ) ≤ 𝑎 ∧ ∀ 𝑒 ∈ ℕ0 ( abs ‘ ( ( coeff ‘ 𝑑 ) ‘ 𝑒 ) ) ≤ 𝑎 ) } ( 𝑐 ‘ 𝑏 ) = 0 } ∈ V
12	11 1	fnmpti	⊢ 𝐻 Fn ℕ0
13		dffn4	⊢ ( 𝐻 Fn ℕ0 ↔ 𝐻 : ℕ0 –onto→ ran 𝐻 )
14	12 13	mpbi	⊢ 𝐻 : ℕ0 –onto→ ran 𝐻
15		fodomnum	⊢ ( ℕ0 ∈ dom card → ( 𝐻 : ℕ0 –onto→ ran 𝐻 → ran 𝐻 ≼ ℕ0 ) )
16	9 14 15	mp2	⊢ ran 𝐻 ≼ ℕ0
17		domentr	⊢ ( ( ran 𝐻 ≼ ℕ0 ∧ ℕ0 ≈ ω ) → ran 𝐻 ≼ ω )
18	16 6 17	mp2an	⊢ ran 𝐻 ≼ ω
19		fvelrnb	⊢ ( 𝐻 Fn ℕ0 → ( 𝑓 ∈ ran 𝐻 ↔ ∃ 𝑔 ∈ ℕ0 ( 𝐻 ‘ 𝑔 ) = 𝑓 ) )
20	12 19	ax-mp	⊢ ( 𝑓 ∈ ran 𝐻 ↔ ∃ 𝑔 ∈ ℕ0 ( 𝐻 ‘ 𝑔 ) = 𝑓 )
21	1	aannenlem1	⊢ ( 𝑔 ∈ ℕ0 → ( 𝐻 ‘ 𝑔 ) ∈ Fin )
22		eleq1	⊢ ( ( 𝐻 ‘ 𝑔 ) = 𝑓 → ( ( 𝐻 ‘ 𝑔 ) ∈ Fin ↔ 𝑓 ∈ Fin ) )
23	21 22	syl5ibcom	⊢ ( 𝑔 ∈ ℕ0 → ( ( 𝐻 ‘ 𝑔 ) = 𝑓 → 𝑓 ∈ Fin ) )
24	23	rexlimiv	⊢ ( ∃ 𝑔 ∈ ℕ0 ( 𝐻 ‘ 𝑔 ) = 𝑓 → 𝑓 ∈ Fin )
25	20 24	sylbi	⊢ ( 𝑓 ∈ ran 𝐻 → 𝑓 ∈ Fin )
26	25	ssriv	⊢ ran 𝐻 ⊆ Fin
27		aasscn	⊢ 𝔸 ⊆ ℂ
28	2 27	eqsstrri	⊢ ∪ ran 𝐻 ⊆ ℂ
29		soss	⊢ ( ∪ ran 𝐻 ⊆ ℂ → ( 𝑓 Or ℂ → 𝑓 Or ∪ ran 𝐻 ) )
30	28 29	ax-mp	⊢ ( 𝑓 Or ℂ → 𝑓 Or ∪ ran 𝐻 )
31		iunfictbso	⊢ ( ( ran 𝐻 ≼ ω ∧ ran 𝐻 ⊆ Fin ∧ 𝑓 Or ∪ ran 𝐻 ) → ∪ ran 𝐻 ≼ ω )
32	18 26 30 31	mp3an12i	⊢ ( 𝑓 Or ℂ → ∪ ran 𝐻 ≼ ω )
33	2 32	eqbrtrid	⊢ ( 𝑓 Or ℂ → 𝔸 ≼ ω )
34		cnso	⊢ ∃ 𝑓 𝑓 Or ℂ
35	33 34	exlimiiv	⊢ 𝔸 ≼ ω
36	5	ensymi	⊢ ω ≈ ℕ
37		domentr	⊢ ( ( 𝔸 ≼ ω ∧ ω ≈ ℕ ) → 𝔸 ≼ ℕ )
38	35 36 37	mp2an	⊢ 𝔸 ≼ ℕ
39	10 27	ssexi	⊢ 𝔸 ∈ V
40		nnssq	⊢ ℕ ⊆ ℚ
41		qssaa	⊢ ℚ ⊆ 𝔸
42	40 41	sstri	⊢ ℕ ⊆ 𝔸
43		ssdomg	⊢ ( 𝔸 ∈ V → ( ℕ ⊆ 𝔸 → ℕ ≼ 𝔸 ) )
44	39 42 43	mp2	⊢ ℕ ≼ 𝔸
45		sbth	⊢ ( ( 𝔸 ≼ ℕ ∧ ℕ ≼ 𝔸 ) → 𝔸 ≈ ℕ )
46	38 44 45	mp2an	⊢ 𝔸 ≈ ℕ