# Metamath Proof Explorer

## 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

### Detailed syntax breakdown

Step Hyp Ref Expression
0 corng ${class}\mathrm{oRing}$
1 vr ${setvar}{r}$
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 ${setvar}{r}$
7 6 5 cfv ${class}{\mathrm{Base}}_{{r}}$
8 vv ${setvar}{v}$
9 c0g ${class}{0}_{𝑔}$
10 6 9 cfv ${class}{0}_{{r}}$
11 vz ${setvar}{z}$
12 cmulr ${class}{\cdot }_{𝑟}$
13 6 12 cfv ${class}{\cdot }_{{r}}$
14 vt ${setvar}{t}$
15 cple ${class}\mathrm{le}$
16 6 15 cfv ${class}{\le }_{{r}}$
17 vl ${setvar}{l}$
18 va ${setvar}{a}$
19 8 cv ${setvar}{v}$
20 vb ${setvar}{b}$
21 11 cv ${setvar}{z}$
22 17 cv ${setvar}{l}$
23 18 cv ${setvar}{a}$
24 21 23 22 wbr ${wff}{z}{l}{a}$
25 20 cv ${setvar}{b}$
26 21 25 22 wbr ${wff}{z}{l}{b}$
27 24 26 wa ${wff}\left({z}{l}{a}\wedge {z}{l}{b}\right)$
28 14 cv ${setvar}{t}$
29 23 25 28 co ${class}\left({a}{t}{b}\right)$
30 21 29 22 wbr ${wff}{z}{l}\left({a}{t}{b}\right)$
31 27 30 wi ${wff}\left(\left({z}{l}{a}\wedge {z}{l}{b}\right)\to {z}{l}\left({a}{t}{b}\right)\right)$
32 31 20 19 wral ${wff}\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({z}{l}{a}\wedge {z}{l}{b}\right)\to {z}{l}\left({a}{t}{b}\right)\right)$
33 32 18 19 wral ${wff}\forall {a}\in {v}\phantom{\rule{.4em}{0ex}}\forall {b}\in {v}\phantom{\rule{.4em}{0ex}}\left(\left({z}{l}{a}\wedge {z}{l}{b}\right)\to {z}{l}\left({a}{t}{b}\right)\right)$
34 33 17 16 wsbc
35 34 14 13 wsbc
36 35 11 10 wsbc
37 36 8 7 wsbc
38 37 1 4 crab
39 0 38 wceq