Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-finext Structured version   Visualization version   GIF version

Definition df-finext 31126
 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
StepHypRef Expression
1 cfinext 31121 . 2 class /FinExt
2 ve . . . . . 6 setvar 𝑒
32cv 1537 . . . . 5 class 𝑒
4 vf . . . . . 6 setvar 𝑓
54cv 1537 . . . . 5 class 𝑓
6 cfldext 31120 . . . . 5 class /FldExt
73, 5, 6wbr 5033 . . . 4 wff 𝑒/FldExt𝑓
8 cextdg 31123 . . . . . 6 class [:]
93, 5, 8co 7139 . . . . 5 class (𝑒[:]𝑓)
10 cn0 11889 . . . . 5 class 0
119, 10wcel 2112 . . . 4 wff (𝑒[:]𝑓) ∈ ℕ0
127, 11wa 399 . . 3 wff (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)
1312, 2, 4copab 5095 . 2 class {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}
141, 13wceq 1538 1 wff /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)}
 Colors of variables: wff setvar class This definition is referenced by:  brfinext  31135
 Copyright terms: Public domain W3C validator