Axiom ax-exfinfld 43220

Description: Existence axiom for finite fields, eventually we want to construct them. (Contributed by metakunt, 13-Jul-2025.)

Assertion

Ref	Expression
ax-exfinfld	⊢ ∀𝑝 ∈ ℙ ∀𝑛 ∈ ℕ ∃𝑘 ∈ Field ((♯‘(Base‘𝑘)) = (𝑝↑𝑛) ∧ (chr‘𝑘) = 𝑝)

Distinct variable group:   𝑛,𝑝,𝑘

Detailed syntax breakdown of Axiom ax-exfinfld

Step	Hyp	Ref	Expression
1		vk	. . . . . . . . 9 setvar 𝑘
2	1	cv 1569	. . . . . . . 8 class 𝑘
3		cbs 17367	. . . . . . . 8 class Base
4	2, 3	cfv 6531	. . . . . . 7 class (Base‘𝑘)
5		chash 14454	. . . . . . 7 class ♯
6	4, 5	cfv 6531	. . . . . 6 class (♯‘(Base‘𝑘))
7		vp	. . . . . . . 8 setvar 𝑝
8	7	cv 1569	. . . . . . 7 class 𝑝
9		vn	. . . . . . . 8 setvar 𝑛
10	9	cv 1569	. . . . . . 7 class 𝑛
11		cexp 14184	. . . . . . 7 class ↑
12	8, 10, 11	co 7412	. . . . . 6 class (𝑝↑𝑛)
13	6, 12	wceq 1570	. . . . 5 wff (♯‘(Base‘𝑘)) = (𝑝↑𝑛)
14		cchr 21787	. . . . . . 7 class chr
15	2, 14	cfv 6531	. . . . . 6 class (chr‘𝑘)
16	15, 8	wceq 1570	. . . . 5 wff (chr‘𝑘) = 𝑝
17	13, 16	wa 401	. . . 4 wff ((♯‘(Base‘𝑘)) = (𝑝↑𝑛) ∧ (chr‘𝑘) = 𝑝)
18		cfield 20961	. . . 4 class Field
19	17, 1, 18	wrex 3087	. . 3 wff ∃𝑘 ∈ Field ((♯‘(Base‘𝑘)) = (𝑝↑𝑛) ∧ (chr‘𝑘) = 𝑝)
20		cn 12316	. . 3 class ℕ
21	19, 9, 20	wral 3077	. 2 wff ∀𝑛 ∈ ℕ ∃𝑘 ∈ Field ((♯‘(Base‘𝑘)) = (𝑝↑𝑛) ∧ (chr‘𝑘) = 𝑝)
22		cprime 16826	. 2 class ℙ
23	21, 7, 22	wral 3077	1 wff ∀𝑝 ∈ ℙ ∀𝑛 ∈ ℕ ∃𝑘 ∈ Field ((♯‘(Base‘𝑘)) = (𝑝↑𝑛) ∧ (chr‘𝑘) = 𝑝)

This axiom is used by:  exfinfldd  43221