Definition df-tsr 18520

Description: Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009.)

Assertion

Ref	Expression
df-tsr	⊢ TosetRel = {𝑟 ∈ PosetRel ∣ (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)}

Detailed syntax breakdown of Definition df-tsr

Step	Hyp	Ref	Expression
1		ctsr 18518	. 2 class TosetRel
2		vr	. . . . . . 7 setvar 𝑟
3	2	cv 1541	. . . . . 6 class 𝑟
4	3	cdm 5677	. . . . 5 class dom 𝑟
5	4, 4	cxp 5675	. . . 4 class (dom 𝑟 × dom 𝑟)
6	3	ccnv 5676	. . . . 5 class ◡𝑟
7	3, 6	cun 3947	. . . 4 class (𝑟 ∪ ◡𝑟)
8	5, 7	wss 3949	. . 3 wff (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)
9		cps 18517	. . 3 class PosetRel
10	8, 2, 9	crab 3433	. 2 class {𝑟 ∈ PosetRel ∣ (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)}
11	1, 10	wceq 1542	1 wff TosetRel = {𝑟 ∈ PosetRel ∣ (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)}

This definition is referenced by:  istsr  18536