Definition df-finext 33749

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

Assertion

Ref	Expression
df-finext	⊢ /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}

Distinct variable group:   𝑒,𝑓

Detailed syntax breakdown of Definition df-finext

Step	Hyp	Ref	Expression
1		cfinext 33745	. 2 class /FinExt
2		ve	. . . . . 6 setvar 𝑒
3	2	cv 1540	. . . . 5 class 𝑒
4		vf	. . . . . 6 setvar 𝑓
5	4	cv 1540	. . . . 5 class 𝑓
6		cfldext 33744	. . . . 5 class /FldExt
7	3, 5, 6	wbr 5096	. . . 4 wff 𝑒/FldExt𝑓
8		cextdg 33746	. . . . . 6 class [:]
9	3, 5, 8	co 7356	. . . . 5 class (𝑒[:]𝑓)
10		cn0 12399	. . . . 5 class ℕ0
11	9, 10	wcel 2113	. . . 4 wff (𝑒[:]𝑓) ∈ ℕ0
12	7, 11	wa 395	. . 3 wff (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)
13	12, 2, 4	copab 5158	. 2 class {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}
14	1, 13	wceq 1541	1 wff /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}

This definition is referenced by:  brfinext  33758  finextfldext  33770