Definition df-algext

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

	Ref	Expression
Assertion	df-algext	$$⊢{/}_{\mathrm{AlgExt}}=\left\{⟨e,f⟩|\left(e{/}_{\mathrm{FldExt}}f\wedge e\mathrm{IntgRing}f={\mathrm{Base}}_e\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		calgext	$$class{/}_{\mathrm{AlgExt}}$$
1		ve	$$setvare$$
2		vf	$$setvarf$$
3	1	cv	$$setvare$$
4		cfldext	$$class{/}_{\mathrm{FldExt}}$$
5	2	cv	$$setvarf$$
6	3 5 4	wbr	$$wffe{/}_{\mathrm{FldExt}}f$$
7		cirng	$$class\mathrm{IntgRing}$$
8	3 5 7	co	$$class\left(e\mathrm{IntgRing}f\right)$$
9		cbs	$$class\mathrm{Base}$$
10	3 9	cfv	$$class{\mathrm{Base}}_e$$
11	8 10	wceq	$$wffe\mathrm{IntgRing}f={\mathrm{Base}}_e$$
12	6 11	wa	$$wff\left(e{/}_{\mathrm{FldExt}}f\wedge e\mathrm{IntgRing}f={\mathrm{Base}}_e\right)$$
13	12 1 2	copab	$$class\left\{⟨e,f⟩|\left(e{/}_{\mathrm{FldExt}}f\wedge e\mathrm{IntgRing}f={\mathrm{Base}}_e\right)\right\}$$
14	0 13	wceq	$$wff{/}_{\mathrm{AlgExt}}=\left\{⟨e,f⟩|\left(e{/}_{\mathrm{FldExt}}f\wedge e\mathrm{IntgRing}f={\mathrm{Base}}_e\right)\right\}$$