Definition df-orng

Description: Define class of all ordered rings. An ordered ring is a ring with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018)

	Ref	Expression
Assertion	df-orng	$$⊢\mathrm{oRing}=\left\{r\in \left(\mathrm{Ring}\cap \mathrm{oGrp}\right)|\underset{\dot{}}{[}{\mathrm{Base}}_r/v\underset{\dot{}}{]}\underset{\dot{}}{[}{0}_r/z\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_r/t\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_r/l\underset{\dot{}}{]}\forall a\in v\forall b\in v\left(\left(zla\wedge zlb\right)\to zl\left(atb\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		corng	$$class\mathrm{oRing}$$
1		vr	$$setvarr$$
2		crg	$$class\mathrm{Ring}$$
3		cogrp	$$class\mathrm{oGrp}$$
4	2 3	cin	$$class\left(\mathrm{Ring}\cap \mathrm{oGrp}\right)$$
5		cbs	$$class\mathrm{Base}$$
6	1	cv	$$setvarr$$
7	6 5	cfv	$$class{\mathrm{Base}}_r$$
8		vv	$$setvarv$$
9		c0g	$$class{0}_{𝑔}$$
10	6 9	cfv	$$class{0}_r$$
11		vz	$$setvarz$$
12		cmulr	$$class{\cdot }_{𝑟}$$
13	6 12	cfv	$$class{\cdot }_r$$
14		vt	$$setvart$$
15		cple	$$class\mathrm{le}$$
16	6 15	cfv	$$class{\le }_r$$
17		vl	$$setvarl$$
18		va	$$setvara$$
19	8	cv	$$setvarv$$
20		vb	$$setvarb$$
21	11	cv	$$setvarz$$
22	17	cv	$$setvarl$$
23	18	cv	$$setvara$$
24	21 23 22	wbr	$$wffzla$$
25	20	cv	$$setvarb$$
26	21 25 22	wbr	$$wffzlb$$
27	24 26	wa	$$wff\left(zla\wedge zlb\right)$$
28	14	cv	$$setvart$$
29	23 25 28	co	$$class\left(atb\right)$$
30	21 29 22	wbr	$$wffzl\left(atb\right)$$
31	27 30	wi	$$wff\left(\left(zla\wedge zlb\right)\to zl\left(atb\right)\right)$$
32	31 20 19	wral	$$wff\forall b\in v\left(\left(zla\wedge zlb\right)\to zl\left(atb\right)\right)$$
33	32 18 19	wral	$$wff\forall a\in v\forall b\in v\left(\left(zla\wedge zlb\right)\to zl\left(atb\right)\right)$$
34	33 17 16	wsbc	$$wff\underset{\dot{}}{[}{\le }_r/l\underset{\dot{}}{]}\forall a\in v\forall b\in v\left(\left(zla\wedge zlb\right)\to zl\left(atb\right)\right)$$
35	34 14 13	wsbc	$$wff\underset{\dot{}}{[}{\cdot }_r/t\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_r/l\underset{\dot{}}{]}\forall a\in v\forall b\in v\left(\left(zla\wedge zlb\right)\to zl\left(atb\right)\right)$$
36	35 11 10	wsbc	$$wff\underset{\dot{}}{[}{0}_r/z\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_r/t\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_r/l\underset{\dot{}}{]}\forall a\in v\forall b\in v\left(\left(zla\wedge zlb\right)\to zl\left(atb\right)\right)$$
37	36 8 7	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_r/v\underset{\dot{}}{]}\underset{\dot{}}{[}{0}_r/z\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_r/t\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_r/l\underset{\dot{}}{]}\forall a\in v\forall b\in v\left(\left(zla\wedge zlb\right)\to zl\left(atb\right)\right)$$
38	37 1 4	crab	$$class\left\{r\in \left(\mathrm{Ring}\cap \mathrm{oGrp}\right)|\underset{\dot{}}{[}{\mathrm{Base}}_r/v\underset{\dot{}}{]}\underset{\dot{}}{[}{0}_r/z\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_r/t\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_r/l\underset{\dot{}}{]}\forall a\in v\forall b\in v\left(\left(zla\wedge zlb\right)\to zl\left(atb\right)\right)\right\}$$
39	0 38	wceq	$$wff\mathrm{oRing}=\left\{r\in \left(\mathrm{Ring}\cap \mathrm{oGrp}\right)|\underset{\dot{}}{[}{\mathrm{Base}}_r/v\underset{\dot{}}{]}\underset{\dot{}}{[}{0}_r/z\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_r/t\underset{\dot{}}{]}\underset{\dot{}}{[}{\le }_r/l\underset{\dot{}}{]}\forall a\in v\forall b\in v\left(\left(zla\wedge zlb\right)\to zl\left(atb\right)\right)\right\}$$