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