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	|- A. p e. Prime A. n e. NN E. k e. Field ( ( # ` ( Base ` k ) ) = ( p ^ n ) /\ ( chr ` k ) = p )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vp	|- p
1		cprime	|- Prime
2		vn	|- n
3		cn	|- NN
4		vk	|- k
5		cfield	|- Field
6		chash	|- #
7		cbs	|- Base
8	4	cv	|- k
9	8 7	cfv	|- ( Base ` k )
10	9 6	cfv	|- ( # ` ( Base ` k ) )
11	0	cv	|- p
12		cexp	|- ^
13	2	cv	|- n
14	11 13 12	co	|- ( p ^ n )
15	10 14	wceq	|- ( # ` ( Base ` k ) ) = ( p ^ n )
16		cchr	|- chr
17	8 16	cfv	|- ( chr ` k )
18	17 11	wceq	|- ( chr ` k ) = p
19	15 18	wa	|- ( ( # ` ( Base ` k ) ) = ( p ^ n ) /\ ( chr ` k ) = p )
20	19 4 5	wrex	|- E. k e. Field ( ( # ` ( Base ` k ) ) = ( p ^ n ) /\ ( chr ` k ) = p )
21	20 2 3	wral	|- A. n e. NN E. k e. Field ( ( # ` ( Base ` k ) ) = ( p ^ n ) /\ ( chr ` k ) = p )
22	21 0 1	wral	|- A. p e. Prime A. n e. NN E. k e. Field ( ( # ` ( Base ` k ) ) = ( p ^ n ) /\ ( chr ` k ) = p )