Definition df-finext

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfinext	⊢ /FinExt
1		ve	⊢ 𝑒
2		vf	⊢ 𝑓
3	1	cv	⊢ 𝑒
4		cfldext	⊢ /FldExt
5	2	cv	⊢ 𝑓
6	3 5 4	wbr	⊢ 𝑒 /FldExt 𝑓
7		cextdg	⊢ [:]
8	3 5 7	co	⊢ ( 𝑒 [:] 𝑓 )
9		cn0	⊢ ℕ0
10	8 9	wcel	⊢ ( 𝑒 [:] 𝑓 ) ∈ ℕ0
11	6 10	wa	⊢ ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 [:] 𝑓 ) ∈ ℕ0 )
12	11 1 2	copab	⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 [:] 𝑓 ) ∈ ℕ0 ) }
13	0 12	wceq	⊢ /FinExt = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 /FldExt 𝑓 ∧ ( 𝑒 [:] 𝑓 ) ∈ ℕ0 ) }