Metamath Proof Explorer


Theorem tosso

Description: Write the totally ordered set structure predicate in terms of the proper class strict order predicate. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses tosso.b B = Base K
tosso.l ˙ = K
tosso.s < ˙ = < K
Assertion tosso K V K Toset < ˙ Or B I B ˙

Proof

Step Hyp Ref Expression
1 tosso.b B = Base K
2 tosso.l ˙ = K
3 tosso.s < ˙ = < K
4 1 2 3 pleval2 K Poset x B y B x ˙ y x < ˙ y x = y
5 4 3expb K Poset x B y B x ˙ y x < ˙ y x = y
6 1 2 3 pleval2 K Poset y B x B y ˙ x y < ˙ x y = x
7 equcom y = x x = y
8 7 orbi2i y < ˙ x y = x y < ˙ x x = y
9 6 8 bitrdi K Poset y B x B y ˙ x y < ˙ x x = y
10 9 3com23 K Poset x B y B y ˙ x y < ˙ x x = y
11 10 3expb K Poset x B y B y ˙ x y < ˙ x x = y
12 5 11 orbi12d K Poset x B y B x ˙ y y ˙ x x < ˙ y x = y y < ˙ x x = y
13 df-3or x < ˙ y x = y y < ˙ x x < ˙ y x = y y < ˙ x
14 or32 x < ˙ y x = y y < ˙ x x < ˙ y y < ˙ x x = y
15 orordir x < ˙ y y < ˙ x x = y x < ˙ y x = y y < ˙ x x = y
16 14 15 bitri x < ˙ y x = y y < ˙ x x < ˙ y x = y y < ˙ x x = y
17 13 16 bitri x < ˙ y x = y y < ˙ x x < ˙ y x = y y < ˙ x x = y
18 12 17 bitr4di K Poset x B y B x ˙ y y ˙ x x < ˙ y x = y y < ˙ x
19 18 2ralbidva K Poset x B y B x ˙ y y ˙ x x B y B x < ˙ y x = y y < ˙ x
20 19 pm5.32i K Poset x B y B x ˙ y y ˙ x K Poset x B y B x < ˙ y x = y y < ˙ x
21 1 2 3 pospo K V K Poset < ˙ Po B I B ˙
22 21 anbi1d K V K Poset x B y B x < ˙ y x = y y < ˙ x < ˙ Po B I B ˙ x B y B x < ˙ y x = y y < ˙ x
23 20 22 syl5bb K V K Poset x B y B x ˙ y y ˙ x < ˙ Po B I B ˙ x B y B x < ˙ y x = y y < ˙ x
24 1 2 istos K Toset K Poset x B y B x ˙ y y ˙ x
25 df-so < ˙ Or B < ˙ Po B x B y B x < ˙ y x = y y < ˙ x
26 25 anbi1i < ˙ Or B I B ˙ < ˙ Po B x B y B x < ˙ y x = y y < ˙ x I B ˙
27 an32 < ˙ Po B x B y B x < ˙ y x = y y < ˙ x I B ˙ < ˙ Po B I B ˙ x B y B x < ˙ y x = y y < ˙ x
28 26 27 bitri < ˙ Or B I B ˙ < ˙ Po B I B ˙ x B y B x < ˙ y x = y y < ˙ x
29 23 24 28 3bitr4g K V K Toset < ˙ Or B I B ˙