This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ Poset | [˙Base f / b]˙ [˙≤ f / r]˙ ∀ x ∈ b ∀ y ∈ b x r y ∨ y r x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctos class Toset
1 vf setvar f
2 cpo class Poset
3 cbs class Base
4 1 cv setvar f
5 4 3 cfv class Base f
6 vb setvar b
7 cple class le
8 4 7 cfv class ≤ f
9 vr setvar r
10 vx setvar x
11 6 cv setvar b
12 vy setvar y
13 10 cv setvar x
14 9 cv setvar r
15 12 cv setvar y
16 13 15 14 wbr wff x r y
17 15 13 14 wbr wff y r x
18 16 17 wo wff x r y ∨ y r x
19 18 12 11 wral wff ∀ y ∈ b x r y ∨ y r x
20 19 10 11 wral wff ∀ x ∈ b ∀ y ∈ b x r y ∨ y r x
21 20 9 8 wsbc wff [˙≤ f / r]˙ ∀ x ∈ b ∀ y ∈ b x r y ∨ y r x
22 21 6 5 wsbc wff [˙Base f / b]˙ [˙≤ f / r]˙ ∀ x ∈ b ∀ y ∈ b x r y ∨ y r x
23 22 1 2 crab class f ∈ Poset | [˙Base f / b]˙ [˙≤ f / r]˙ ∀ x ∈ b ∀ y ∈ b x r y ∨ y r x
24 0 23 wceq wff Toset = f ∈ Poset | [˙Base f / b]˙ [˙≤ f / r]˙ ∀ x ∈ b ∀ y ∈ b x r y ∨ y r x