Definition df-orng 32415

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 = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}

Distinct variable group:   𝑎,𝑏,𝑙,𝑟,𝑡,𝑣,𝑧

Detailed syntax breakdown of Definition df-orng

Step	Hyp	Ref	Expression
1		corng 32413	. 2 class oRing
2		vz	. . . . . . . . . . . . 13 setvar 𝑧
3	2	cv 1541	. . . . . . . . . . . 12 class 𝑧
4		va	. . . . . . . . . . . . 13 setvar 𝑎
5	4	cv 1541	. . . . . . . . . . . 12 class 𝑎
6		vl	. . . . . . . . . . . . 13 setvar 𝑙
7	6	cv 1541	. . . . . . . . . . . 12 class 𝑙
8	3, 5, 7	wbr 5149	. . . . . . . . . . 11 wff 𝑧𝑙𝑎
9		vb	. . . . . . . . . . . . 13 setvar 𝑏
10	9	cv 1541	. . . . . . . . . . . 12 class 𝑏
11	3, 10, 7	wbr 5149	. . . . . . . . . . 11 wff 𝑧𝑙𝑏
12	8, 11	wa 397	. . . . . . . . . 10 wff (𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏)
13		vt	. . . . . . . . . . . . 13 setvar 𝑡
14	13	cv 1541	. . . . . . . . . . . 12 class 𝑡
15	5, 10, 14	co 7409	. . . . . . . . . . 11 class (𝑎𝑡𝑏)
16	3, 15, 7	wbr 5149	. . . . . . . . . 10 wff 𝑧𝑙(𝑎𝑡𝑏)
17	12, 16	wi 4	. . . . . . . . 9 wff ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
18		vv	. . . . . . . . . 10 setvar 𝑣
19	18	cv 1541	. . . . . . . . 9 class 𝑣
20	17, 9, 19	wral 3062	. . . . . . . 8 wff ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
21	20, 4, 19	wral 3062	. . . . . . 7 wff ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
22		vr	. . . . . . . . 9 setvar 𝑟
23	22	cv 1541	. . . . . . . 8 class 𝑟
24		cple 17204	. . . . . . . 8 class le
25	23, 24	cfv 6544	. . . . . . 7 class (le‘𝑟)
26	21, 6, 25	wsbc 3778	. . . . . 6 wff [(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
27		cmulr 17198	. . . . . . 7 class .r
28	23, 27	cfv 6544	. . . . . 6 class (.r‘𝑟)
29	26, 13, 28	wsbc 3778	. . . . 5 wff [(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
30		c0g 17385	. . . . . 6 class 0g
31	23, 30	cfv 6544	. . . . 5 class (0g‘𝑟)
32	29, 2, 31	wsbc 3778	. . . 4 wff [(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
33		cbs 17144	. . . . 5 class Base
34	23, 33	cfv 6544	. . . 4 class (Base‘𝑟)
35	32, 18, 34	wsbc 3778	. . 3 wff [(Base‘𝑟) / 𝑣][(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))
36		crg 20056	. . . 4 class Ring
37		cogrp 32216	. . . 4 class oGrp
38	36, 37	cin 3948	. . 3 class (Ring ∩ oGrp)
39	35, 22, 38	crab 3433	. 2 class {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}
40	1, 39	wceq 1542	1 wff oRing = {𝑟 ∈ (Ring ∩ oGrp) ∣ [(Base‘𝑟) / 𝑣][(0g‘𝑟) / 𝑧][(.r‘𝑟) / 𝑡][(le‘𝑟) / 𝑙]∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ((𝑧𝑙𝑎 ∧ 𝑧𝑙𝑏) → 𝑧𝑙(𝑎𝑡𝑏))}

This definition is referenced by:  isorng  32417