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 = { 𝑓 ∈ Poset ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctos ⊢ Toset
1 vf ⊢ 𝑓
2 cpo ⊢ Poset
3 cbs ⊢ Base
4 1 cv ⊢ 𝑓
5 4 3 cfv ⊢ ( Base ‘ 𝑓 )
6 vb ⊢ 𝑏
7 cple ⊢ le
8 4 7 cfv ⊢ ( le ‘ 𝑓 )
9 vr ⊢ 𝑟
10 vx ⊢ 𝑥
11 6 cv ⊢ 𝑏
12 vy ⊢ 𝑦
13 10 cv ⊢ 𝑥
14 9 cv ⊢ 𝑟
15 12 cv ⊢ 𝑦
16 13 15 14 wbr ⊢ 𝑥 𝑟 𝑦
17 15 13 14 wbr ⊢ 𝑦 𝑟 𝑥
18 16 17 wo ⊢ ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 )
19 18 12 11 wral ⊢ ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 )
20 19 10 11 wral ⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 )
21 20 9 8 wsbc ⊢ [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 )
22 21 6 5 wsbc ⊢ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 )
23 22 1 2 crab ⊢ { 𝑓 ∈ Poset ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) }
24 0 23 wceq ⊢ Toset = { 𝑓 ∈ Poset ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) }