df-finext

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

		Ref	Expression
	Assertion	df-finext	$⊢ /_{FinExt} = \{⟨e, f⟩ \| (e /_{FldExt} f \land e [. : .] f \in ℕ_{0})\}$

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

Metamath Proof Explorer