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}{\mathrm{Base}}_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		cbs	$$class\mathrm{Base}$$
9	5 8	cfv	$$class{\mathrm{Base}}_f$$
10	3 9 7	co	$$class\left(e\mathrm{IntgRing}{\mathrm{Base}}_f\right)$$
11	3 8	cfv	$$class{\mathrm{Base}}_e$$
12	10 11	wceq	$$wffe\mathrm{IntgRing}{\mathrm{Base}}_f={\mathrm{Base}}_e$$
13	6 12	wa	$$wff\left(e{/}_{\mathrm{FldExt}}f\wedge e\mathrm{IntgRing}{\mathrm{Base}}_f={\mathrm{Base}}_e\right)$$
14	13 1 2	copab	$$class\left\{⟨e,f⟩|\left(e{/}_{\mathrm{FldExt}}f\wedge e\mathrm{IntgRing}{\mathrm{Base}}_f={\mathrm{Base}}_e\right)\right\}$$
15	0 14	wceq	$$wff{/}_{\mathrm{AlgExt}}=\left\{⟨e,f⟩|\left(e{/}_{\mathrm{FldExt}}f\wedge e\mathrm{IntgRing}{\mathrm{Base}}_f={\mathrm{Base}}_e\right)\right\}$$