Definition df-finext 31056

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 31051	. 2 class /FinExt
2		ve	. . . . . 6 setvar 𝑒
3	2	cv 1535	. . . . 5 class 𝑒
4		vf	. . . . . 6 setvar 𝑓
5	4	cv 1535	. . . . 5 class 𝑓
6		cfldext 31050	. . . . 5 class /FldExt
7	3, 5, 6	wbr 5059	. . . 4 wff 𝑒/FldExt𝑓
8		cextdg 31053	. . . . . 6 class [:]
9	3, 5, 8	co 7149	. . . . 5 class (𝑒[:]𝑓)
10		cn0 11891	. . . . 5 class ℕ0
11	9, 10	wcel 2113	. . . 4 wff (𝑒[:]𝑓) ∈ ℕ0
12	7, 11	wa 398	. . 3 wff (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)
13	12, 2, 4	copab 5121	. 2 class {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}
14	1, 13	wceq 1536	1 wff /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}

This definition is referenced by:  brfinext  31065