aannenlem3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > aannenlem3		Structured version Visualization version GIF version

Theorem aannenlem3 24023

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

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

**Assertion**
Ref	Expression
aannenlem3	⊢ 𝔸 ≈ ℕ

Distinct variable group: 𝑎,𝑏,𝑐,𝑑,𝑒 Allowed substitution hints: 𝐻(𝑒,𝑎,𝑏,𝑐,𝑑)

Proof of Theorem aannenlem3 Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		aannenlem.a	. . . . . 6 ⊢ 𝐻 = (𝑎 ∈ ℕ₀ ↦ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0})
2	1	aannenlem2 24022	. . . . 5 ⊢ 𝔸 = ∪ ran 𝐻
3		omelon 8503	. . . . . . . . . 10 ⊢ ω ∈ On
4		nn0ennn 12734	. . . . . . . . . . . 12 ⊢ ℕ₀ ≈ ℕ
5		nnenom 12735	. . . . . . . . . . . 12 ⊢ ℕ ≈ ω
6	4, 5	entri 7970	. . . . . . . . . . 11 ⊢ ℕ₀ ≈ ω
7	6	ensymi 7966	. . . . . . . . . 10 ⊢ ω ≈ ℕ₀
8		isnumi 8732	. . . . . . . . . 10 ⊢ ((ω ∈ On ∧ ω ≈ ℕ₀) → ℕ₀ ∈ dom card)
9	3, 7, 8	mp2an 707	. . . . . . . . 9 ⊢ ℕ₀ ∈ dom card
10		cnex 9977	. . . . . . . . . . . 12 ⊢ ℂ ∈ V
11	10	rabex 4783	. . . . . . . . . . 11 ⊢ {𝑏 ∈ ℂ ∣ ∃𝑐 ∈ {𝑑 ∈ (Poly‘ℤ) ∣ (𝑑 ≠ 0_𝑝 ∧ (deg‘𝑑) ≤ 𝑎 ∧ ∀𝑒 ∈ ℕ₀ (abs‘((coeff‘𝑑)‘𝑒)) ≤ 𝑎)} (𝑐‘𝑏) = 0} ∈ V
12	11, 1	fnmpti 5989	. . . . . . . . . 10 ⊢ 𝐻 Fn ℕ₀
13		dffn4 6088	. . . . . . . . . 10 ⊢ (𝐻 Fn ℕ₀ ↔ 𝐻:ℕ₀–onto→ran 𝐻)
14	12, 13	mpbi 220	. . . . . . . . 9 ⊢ 𝐻:ℕ₀–onto→ran 𝐻
15		fodomnum 8840	. . . . . . . . 9 ⊢ (ℕ₀ ∈ dom card → (𝐻:ℕ₀–onto→ran 𝐻 → ran 𝐻 ≼ ℕ₀))
16	9, 14, 15	mp2 9	. . . . . . . 8 ⊢ ran 𝐻 ≼ ℕ₀
17		domentr 7975	. . . . . . . 8 ⊢ ((ran 𝐻 ≼ ℕ₀ ∧ ℕ₀ ≈ ω) → ran 𝐻 ≼ ω)
18	16, 6, 17	mp2an 707	. . . . . . 7 ⊢ ran 𝐻 ≼ ω
19	18	a1i 11	. . . . . 6 ⊢ (𝑓 Or ℂ → ran 𝐻 ≼ ω)
20		fvelrnb 6210	. . . . . . . . . 10 ⊢ (𝐻 Fn ℕ₀ → (𝑓 ∈ ran 𝐻 ↔ ∃𝑔 ∈ ℕ₀ (𝐻‘𝑔) = 𝑓))
21	12, 20	ax-mp 5	. . . . . . . . 9 ⊢ (𝑓 ∈ ran 𝐻 ↔ ∃𝑔 ∈ ℕ₀ (𝐻‘𝑔) = 𝑓)
22	1	aannenlem1 24021	. . . . . . . . . . 11 ⊢ (𝑔 ∈ ℕ₀ → (𝐻‘𝑔) ∈ Fin)
23		eleq1 2686	. . . . . . . . . . 11 ⊢ ((𝐻‘𝑔) = 𝑓 → ((𝐻‘𝑔) ∈ Fin ↔ 𝑓 ∈ Fin))
24	22, 23	syl5ibcom 235	. . . . . . . . . 10 ⊢ (𝑔 ∈ ℕ₀ → ((𝐻‘𝑔) = 𝑓 → 𝑓 ∈ Fin))
25	24	rexlimiv 3022	. . . . . . . . 9 ⊢ (∃𝑔 ∈ ℕ₀ (𝐻‘𝑔) = 𝑓 → 𝑓 ∈ Fin)
26	21, 25	sylbi 207	. . . . . . . 8 ⊢ (𝑓 ∈ ran 𝐻 → 𝑓 ∈ Fin)
27	26	ssriv 3592	. . . . . . 7 ⊢ ran 𝐻 ⊆ Fin
28	27	a1i 11	. . . . . 6 ⊢ (𝑓 Or ℂ → ran 𝐻 ⊆ Fin)
29		aasscn 24011	. . . . . . . 8 ⊢ 𝔸 ⊆ ℂ
30	2, 29	eqsstr3i 3621	. . . . . . 7 ⊢ ∪ ran 𝐻 ⊆ ℂ
31		soss 5023	. . . . . . 7 ⊢ (∪ ran 𝐻 ⊆ ℂ → (𝑓 Or ℂ → 𝑓 Or ∪ ran 𝐻))
32	30, 31	ax-mp 5	. . . . . 6 ⊢ (𝑓 Or ℂ → 𝑓 Or ∪ ran 𝐻)
33		iunfictbso 8897	. . . . . 6 ⊢ ((ran 𝐻 ≼ ω ∧ ran 𝐻 ⊆ Fin ∧ 𝑓 Or ∪ ran 𝐻) → ∪ ran 𝐻 ≼ ω)
34	19, 28, 32, 33	syl3anc 1323	. . . . 5 ⊢ (𝑓 Or ℂ → ∪ ran 𝐻 ≼ ω)
35	2, 34	syl5eqbr 4658	. . . 4 ⊢ (𝑓 Or ℂ → 𝔸 ≼ ω)
36		cnso 14920	. . . 4 ⊢ ∃𝑓 𝑓 Or ℂ
37	35, 36	exlimiiv 1856	. . 3 ⊢ 𝔸 ≼ ω
38	5	ensymi 7966	. . 3 ⊢ ω ≈ ℕ
39		domentr 7975	. . 3 ⊢ ((𝔸 ≼ ω ∧ ω ≈ ℕ) → 𝔸 ≼ ℕ)
40	37, 38, 39	mp2an 707	. 2 ⊢ 𝔸 ≼ ℕ
41	10, 29	ssexi 4773	. . 3 ⊢ 𝔸 ∈ V
42		nnssq 11757	. . . 4 ⊢ ℕ ⊆ ℚ
43		qssaa 24017	. . . 4 ⊢ ℚ ⊆ 𝔸
44	42, 43	sstri 3597	. . 3 ⊢ ℕ ⊆ 𝔸
45		ssdomg 7961	. . 3 ⊢ (𝔸 ∈ V → (ℕ ⊆ 𝔸 → ℕ ≼ 𝔸))
46	41, 44, 45	mp2 9	. 2 ⊢ ℕ ≼ 𝔸
47		sbth 8040	. 2 ⊢ ((𝔸 ≼ ℕ ∧ ℕ ≼ 𝔸) → 𝔸 ≈ ℕ)
48	40, 46, 47	mp2an 707	1 ⊢ 𝔸 ≈ ℕ

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ w3a 1036 = wceq 1480 ∈ wcel 1987 ≠ wne 2790 ∀wral 2908 ∃wrex 2909 {crab 2912 Vcvv 3190 ⊆ wss 3560 ∪ cuni 4409 class class class wbr 4623 ↦ cmpt 4683 Or wor 5004 dom cdm 5084 ran crn 5085 Oncon0 5692 Fn wfn 5852 –onto→wfo 5855 ‘cfv 5857 ωcom 7027 ≈ cen 7912 ≼ cdom 7913 Fincfn 7915 cardccrd 8721 ℂcc 9894 0cc0 9896 ≤ cle 10035 ℕcn 10980 ℕ₀cn0 11252 ℤcz 11337 ℚcq 11748 abscabs 13924 0_𝑝c0p 23376 Polycply 23878 coeffccoe 23880 degcdgr 23881 𝔸caa 24007

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-rep 4741 ax-sep 4751 ax-nul 4759 ax-pow 4813 ax-pr 4877 ax-un 6914 ax-inf2 8498 ax-cnex 9952 ax-resscn 9953 ax-1cn 9954 ax-icn 9955 ax-addcl 9956 ax-addrcl 9957 ax-mulcl 9958 ax-mulrcl 9959 ax-mulcom 9960 ax-addass 9961 ax-mulass 9962 ax-distr 9963 ax-i2m1 9964 ax-1ne0 9965 ax-1rid 9966 ax-rnegex 9967 ax-rrecex 9968 ax-cnre 9969 ax-pre-lttri 9970 ax-pre-lttrn 9971 ax-pre-ltadd 9972 ax-pre-mulgt0 9973 ax-pre-sup 9974 ax-addf 9975

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-fal 1486 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-nel 2894 df-ral 2913 df-rex 2914 df-reu 2915 df-rmo 2916 df-rab 2917 df-v 3192 df-sbc 3423 df-csb 3520 df-dif 3563 df-un 3565 df-in 3567 df-ss 3574 df-pss 3576 df-nul 3898 df-if 4065 df-pw 4138 df-sn 4156 df-pr 4158 df-tp 4160 df-op 4162 df-uni 4410 df-int 4448 df-iun 4494 df-br 4624 df-opab 4684 df-mpt 4685 df-tr 4723 df-eprel 4995 df-id 4999 df-po 5005 df-so 5006 df-fr 5043 df-se 5044 df-we 5045 df-xp 5090 df-rel 5091 df-cnv 5092 df-co 5093 df-dm 5094 df-rn 5095 df-res 5096 df-ima 5097 df-pred 5649 df-ord 5695 df-on 5696 df-lim 5697 df-suc 5698 df-iota 5820 df-fun 5859 df-fn 5860 df-f 5861 df-f1 5862 df-fo 5863 df-f1o 5864 df-fv 5865 df-isom 5866 df-riota 6576 df-ov 6618 df-oprab 6619 df-mpt2 6620 df-of 6862 df-om 7028 df-1st 7128 df-2nd 7129 df-wrecs 7367 df-recs 7428 df-rdg 7466 df-1o 7520 df-2o 7521 df-oadd 7524 df-omul 7525 df-er 7702 df-map 7819 df-pm 7820 df-en 7916 df-dom 7917 df-sdom 7918 df-fin 7919 df-sup 8308 df-inf 8309 df-oi 8375 df-card 8725 df-acn 8728 df-cda 8950 df-pnf 10036 df-mnf 10037 df-xr 10038 df-ltxr 10039 df-le 10040 df-sub 10228 df-neg 10229 df-div 10645 df-nn 10981 df-2 11039 df-3 11040 df-n0 11253 df-xnn0 11324 df-z 11338 df-uz 11648 df-q 11749 df-rp 11793 df-ico 12139 df-icc 12140 df-fz 12285 df-fzo 12423 df-fl 12549 df-mod 12625 df-seq 12758 df-exp 12817 df-hash 13074 df-cj 13789 df-re 13790 df-im 13791 df-sqrt 13925 df-abs 13926 df-limsup 14152 df-clim 14169 df-rlim 14170 df-sum 14367 df-0p 23377 df-ply 23882 df-idp 23883 df-coe 23884 df-dgr 23885 df-quot 23984 df-aa 24008

This theorem is referenced by: aannen 24024

W3C validator