Definition df-tsr

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctsr	⊢ TosetRel
1		vr	⊢ 𝑟
2		cps	⊢ PosetRel
3	1	cv	⊢ 𝑟
4	3	cdm	⊢ dom 𝑟
5	4 4	cxp	⊢ ( dom 𝑟 × dom 𝑟 )
6	3	ccnv	⊢ ◡ 𝑟
7	3 6	cun	⊢ ( 𝑟 ∪ ◡ 𝑟 )
8	5 7	wss	⊢ ( dom 𝑟 × dom 𝑟 ) ⊆ ( 𝑟 ∪ ◡ 𝑟 )
9	8 1 2	crab	⊢ { 𝑟 ∈ PosetRel ∣ ( dom 𝑟 × dom 𝑟 ) ⊆ ( 𝑟 ∪ ◡ 𝑟 ) }
10	0 9	wceq	⊢ TosetRel = { 𝑟 ∈ PosetRel ∣ ( dom 𝑟 × dom 𝑟 ) ⊆ ( 𝑟 ∪ ◡ 𝑟 ) }