Metamath Proof Explorer

Definition df-toset

Description: Define the class of totally ordered sets (tosets). (Contributed by FL, 17-Nov-2014)

Ref Expression
Assertion df-toset 
|- Toset = { f e. Poset | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctos 
 |-  Toset
1 vf 
 |-  f
2 cpo 
 |-  Poset
3 cbs 
 |-  Base
4 1 cv 
 |-  f
5 4 3 cfv 
 |-  ( Base ` f )
6 vb 
 |-  b
7 cple 
 |-  le
8 4 7 cfv 
 |-  ( le ` f )
9 vr 
 |-  r
10 vx 
 |-  x
11 6 cv 
 |-  b
12 vy 
 |-  y
13 10 cv 
 |-  x
14 9 cv 
 |-  r
15 12 cv 
 |-  y
16 13 15 14 wbr 
 |-  x r y
17 15 13 14 wbr 
 |-  y r x
18 16 17 wo 
 |-  ( x r y \/ y r x )
19 18 12 11 wral 
 |-  A. y e. b ( x r y \/ y r x )
20 19 10 11 wral 
 |-  A. x e. b A. y e. b ( x r y \/ y r x )
21 20 9 8 wsbc 
 |-  [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x )
22 21 6 5 wsbc 
 |-  [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x )
23 22 1 2 crab 
 |-  { f e. Poset | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x ) }
24 0 23 wceq 
 |-  Toset = { f e. Poset | [. ( Base ` f ) / b ]. [. ( le ` f ) / r ]. A. x e. b A. y e. b ( x r y \/ y r x ) }