Axiom ax-exfinfld

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vp	⊢ 𝑝
1		cprime	⊢ ℙ
2		vn	⊢ 𝑛
3		cn	⊢ ℕ
4		vk	⊢ 𝑘
5		cfield	⊢ Field
6		chash	⊢ ♯
7		cbs	⊢ Base
8	4	cv	⊢ 𝑘
9	8 7	cfv	⊢ ( Base ‘ 𝑘 )
10	9 6	cfv	⊢ ( ♯ ‘ ( Base ‘ 𝑘 ) )
11	0	cv	⊢ 𝑝
12		cexp	⊢ ↑
13	2	cv	⊢ 𝑛
14	11 13 12	co	⊢ ( 𝑝 ↑ 𝑛 )
15	10 14	wceq	⊢ ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑝 ↑ 𝑛 )
16		cchr	⊢ chr
17	8 16	cfv	⊢ ( chr ‘ 𝑘 )
18	17 11	wceq	⊢ ( chr ‘ 𝑘 ) = 𝑝
19	15 18	wa	⊢ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑝 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑝 )
20	19 4 5	wrex	⊢ ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑝 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑝 )
21	20 2 3	wral	⊢ ∀ 𝑛 ∈ ℕ ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑝 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑝 )
22	21 0 1	wral	⊢ ∀ 𝑝 ∈ ℙ ∀ 𝑛 ∈ ℕ ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑝 ↑ 𝑛 ) ∧ ( chr ‘ 𝑘 ) = 𝑝 )