Definition df-finext 34042

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 34038	. 2 class /FinExt
2		ve	. . . . . 6 setvar 𝑒
3	2	cv 1569	. . . . 5 class 𝑒
4		vf	. . . . . 6 setvar 𝑓
5	4	cv 1569	. . . . 5 class 𝑓
6		cfldext 34037	. . . . 5 class /FldExt
7	3, 5, 6	wbr 5109	. . . 4 wff 𝑒/FldExt𝑓
8		cextdg 34039	. . . . . 6 class [:]
9	3, 5, 8	co 7410	. . . . 5 class (𝑒[:]𝑓)
10		cn0 12508	. . . . 5 class ℕ0
11	9, 10	wcel 2143	. . . 4 wff (𝑒[:]𝑓) ∈ ℕ0
12	7, 11	wa 400	. . 3 wff (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)
13	12, 2, 4	copab 5173	. 2 class {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}
14	1, 13	wceq 1570	1 wff /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}

This definition is used by:  brfinext  34051  finextfldext  34063