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	$$⊢\forall p\in \mathbb{P}\forall n\in \mathbb{N}\exists k\in \mathrm{Field}\left(\left|{\mathrm{Base}}_k\right|=p^n\wedge \mathrm{chr}\left(k\right)=p\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vp	$$setvarp$$
1		cprime	$$class\mathbb{P}$$
2		vn	$$setvarn$$
3		cn	$$class\mathbb{N}$$
4		vk	$$setvark$$
5		cfield	$$class\mathrm{Field}$$
6		chash	$$class\left|.\right|$$
7		cbs	$$class\mathrm{Base}$$
8	4	cv	$$setvark$$
9	8 7	cfv	$$class{\mathrm{Base}}_k$$
10	9 6	cfv	$$class\left|{\mathrm{Base}}_k\right|$$
11	0	cv	$$setvarp$$
12		cexp	$$class^$$
13	2	cv	$$setvarn$$
14	11 13 12	co	$$class{p}^n$$
15	10 14	wceq	$$wff\left|{\mathrm{Base}}_k\right|=p^n$$
16		cchr	$$class\mathrm{chr}$$
17	8 16	cfv	$$class\mathrm{chr}\left(k\right)$$
18	17 11	wceq	$$wff\mathrm{chr}\left(k\right)=p$$
19	15 18	wa	$$wff\left(\left|{\mathrm{Base}}_k\right|=p^n\wedge \mathrm{chr}\left(k\right)=p\right)$$
20	19 4 5	wrex	$$wff\exists k\in \mathrm{Field}\left(\left|{\mathrm{Base}}_k\right|=p^n\wedge \mathrm{chr}\left(k\right)=p\right)$$
21	20 2 3	wral	$$wff\forall n\in \mathbb{N}\exists k\in \mathrm{Field}\left(\left|{\mathrm{Base}}_k\right|=p^n\wedge \mathrm{chr}\left(k\right)=p\right)$$
22	21 0 1	wral	$$wff\forall p\in \mathbb{P}\forall n\in \mathbb{N}\exists k\in \mathrm{Field}\left(\left|{\mathrm{Base}}_k\right|=p^n\wedge \mathrm{chr}\left(k\right)=p\right)$$