Definition df-finext

Description: Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023)

	Ref	Expression
Assertion	df-finext	$$⊢{/}_{\mathrm{FinExt}}=\left\{⟨e,f⟩|\left(e{/}_{\mathrm{FldExt}}f\wedge e\left[.:.\right]f\in {\mathbb{N}}_0\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfinext	$$class{/}_{\mathrm{FinExt}}$$
1		ve	$$setvare$$
2		vf	$$setvarf$$
3	1	cv	$$setvare$$
4		cfldext	$$class{/}_{\mathrm{FldExt}}$$
5	2	cv	$$setvarf$$
6	3 5 4	wbr	$$wffe{/}_{\mathrm{FldExt}}f$$
7		cextdg	$$class\left[.:.\right]$$
8	3 5 7	co
9		cn0	$$class{\mathbb{N}}_0$$
10	8 9	wcel	$$wffe\left[.:.\right]f\in {\mathbb{N}}_0$$
11	6 10	wa	$$wff\left(e{/}_{\mathrm{FldExt}}f\wedge e\left[.:.\right]f\in {\mathbb{N}}_0\right)$$
12	11 1 2	copab	$$class\left\{⟨e,f⟩|\left(e{/}_{\mathrm{FldExt}}f\wedge e\left[.:.\right]f\in {\mathbb{N}}_0\right)\right\}$$
13	0 12	wceq	$$wff{/}_{\mathrm{FinExt}}=\left\{⟨e,f⟩|\left(e{/}_{\mathrm{FldExt}}f\wedge e\left[.:.\right]f\in {\mathbb{N}}_0\right)\right\}$$