Definition df-finext 33684

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 33679	. 2 class /FinExt
2		ve	. . . . . 6 setvar 𝑒
3	2	cv 1539	. . . . 5 class 𝑒
4		vf	. . . . . 6 setvar 𝑓
5	4	cv 1539	. . . . 5 class 𝑓
6		cfldext 33678	. . . . 5 class /FldExt
7	3, 5, 6	wbr 5119	. . . 4 wff 𝑒/FldExt𝑓
8		cextdg 33681	. . . . . 6 class [:]
9	3, 5, 8	co 7405	. . . . 5 class (𝑒[:]𝑓)
10		cn0 12501	. . . . 5 class ℕ0
11	9, 10	wcel 2108	. . . 4 wff (𝑒[:]𝑓) ∈ ℕ0
12	7, 11	wa 395	. . 3 wff (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)
13	12, 2, 4	copab 5181	. 2 class {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}
14	1, 13	wceq 1540	1 wff /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}

This definition is referenced by:  brfinext  33694