Definition df-orng 29797

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.)

Assertion

Ref	Expression
df-orng	|- oRing = { r e. ( Ring i^i oGrp ) | [. ( Base ` r ) / v ]. [. ( 0g ` r ) / z ]. [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) ) }

Distinct variable group:   a, b, l, r, t, v, z

Detailed syntax breakdown of Definition df-orng

Step	Hyp	Ref	Expression
1		corng 29795	. 2 class oRing
2		vz	. . . . . . . . . . . . 13 setvar z
3	2	cv 1482	. . . . . . . . . . . 12 class z
4		va	. . . . . . . . . . . . 13 setvar a
5	4	cv 1482	. . . . . . . . . . . 12 class a
6		vl	. . . . . . . . . . . . 13 setvar l
7	6	cv 1482	. . . . . . . . . . . 12 class l
8	3, 5, 7	wbr 4653	. . . . . . . . . . 11 wff z l a
9		vb	. . . . . . . . . . . . 13 setvar b
10	9	cv 1482	. . . . . . . . . . . 12 class b
11	3, 10, 7	wbr 4653	. . . . . . . . . . 11 wff z l b
12	8, 11	wa 384	. . . . . . . . . 10 wff ( z l a /\ z l b )
13		vt	. . . . . . . . . . . . 13 setvar t
14	13	cv 1482	. . . . . . . . . . . 12 class t
15	5, 10, 14	co 6650	. . . . . . . . . . 11 class ( a t b )
16	3, 15, 7	wbr 4653	. . . . . . . . . 10 wff z l ( a t b )
17	12, 16	wi 4	. . . . . . . . 9 wff ( ( z l a /\ z l b ) -> z l ( a t b ) )
18		vv	. . . . . . . . . 10 setvar v
19	18	cv 1482	. . . . . . . . 9 class v
20	17, 9, 19	wral 2912	. . . . . . . 8 wff A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) )
21	20, 4, 19	wral 2912	. . . . . . 7 wff A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) )
22		vr	. . . . . . . . 9 setvar r
23	22	cv 1482	. . . . . . . 8 class r
24		cple 15948	. . . . . . . 8 class le
25	23, 24	cfv 5888	. . . . . . 7 class ( le ` r )
26	21, 6, 25	wsbc 3435	. . . . . 6 wff [. ( le ` r ) / l ]. A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) )
27		cmulr 15942	. . . . . . 7 class .r
28	23, 27	cfv 5888	. . . . . 6 class ( .r ` r )
29	26, 13, 28	wsbc 3435	. . . . 5 wff [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) )
30		c0g 16100	. . . . . 6 class 0g
31	23, 30	cfv 5888	. . . . 5 class ( 0g ` r )
32	29, 2, 31	wsbc 3435	. . . 4 wff [. ( 0g ` r ) / z ]. [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) )
33		cbs 15857	. . . . 5 class Base
34	23, 33	cfv 5888	. . . 4 class ( Base ` r )
35	32, 18, 34	wsbc 3435	. . 3 wff [. ( Base ` r ) / v ]. [. ( 0g ` r ) / z ]. [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) )
36		crg 18547	. . . 4 class Ring
37		cogrp 29698	. . . 4 class oGrp
38	36, 37	cin 3573	. . 3 class ( Ring i^i oGrp )
39	35, 22, 38	crab 2916	. 2 class { r e. ( Ring i^i oGrp ) | [. ( Base ` r ) / v ]. [. ( 0g ` r ) / z ]. [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) ) }
40	1, 39	wceq 1483	1 wff oRing = { r e. ( Ring i^i oGrp ) | [. ( Base ` r ) / v ]. [. ( 0g ` r ) / z ]. [. ( .r ` r ) / t ]. [. ( le ` r ) / l ]. A. a e. v A. b e. v ( ( z l a /\ z l b ) -> z l ( a t b ) ) }

This definition is referenced by:  isorng  29799