Definition df-finext

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

	Ref	Expression
Assertion	df-finext	|- /FinExt = { <. e , f >. | ( e /FldExt f /\ ( e [:] f ) e. NN0 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfinext	|- /FinExt
1		ve	|- e
2		vf	|- f
3	1	cv	|- e
4		cfldext	|- /FldExt
5	2	cv	|- f
6	3 5 4	wbr	|- e /FldExt f
7		cextdg	|- [:]
8	3 5 7	co	|- ( e [:] f )
9		cn0	|- NN0
10	8 9	wcel	|- ( e [:] f ) e. NN0
11	6 10	wa	|- ( e /FldExt f /\ ( e [:] f ) e. NN0 )
12	11 1 2	copab	|- { <. e , f >. | ( e /FldExt f /\ ( e [:] f ) e. NN0 ) }
13	0 12	wceq	|- /FinExt = { <. e , f >. | ( e /FldExt f /\ ( e [:] f ) e. NN0 ) }