Theorem solin

Description: A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996)

	Ref	Expression
Assertion	solin	|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C \/ B = C \/ C R B ) )

Proof

Step	Hyp	Ref	Expression
1		breq1	|- ( x = B -> ( x R y <-> B R y ) )
2		eqeq1	|- ( x = B -> ( x = y <-> B = y ) )
3		breq2	|- ( x = B -> ( y R x <-> y R B ) )
4	1 2 3	3orbi123d	|- ( x = B -> ( ( x R y \/ x = y \/ y R x ) <-> ( B R y \/ B = y \/ y R B ) ) )
5	4	imbi2d	|- ( x = B -> ( ( R Or A -> ( x R y \/ x = y \/ y R x ) ) <-> ( R Or A -> ( B R y \/ B = y \/ y R B ) ) ) )
6		breq2	|- ( y = C -> ( B R y <-> B R C ) )
7		eqeq2	|- ( y = C -> ( B = y <-> B = C ) )
8		breq1	|- ( y = C -> ( y R B <-> C R B ) )
9	6 7 8	3orbi123d	|- ( y = C -> ( ( B R y \/ B = y \/ y R B ) <-> ( B R C \/ B = C \/ C R B ) ) )
10	9	imbi2d	|- ( y = C -> ( ( R Or A -> ( B R y \/ B = y \/ y R B ) ) <-> ( R Or A -> ( B R C \/ B = C \/ C R B ) ) ) )
11		df-so	|- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
12		rsp2	|- ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) -> ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) ) )
13	11 12	simplbiim	|- ( R Or A -> ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) ) )
14	13	com12	|- ( ( x e. A /\ y e. A ) -> ( R Or A -> ( x R y \/ x = y \/ y R x ) ) )
15	5 10 14	vtocl2ga	|- ( ( B e. A /\ C e. A ) -> ( R Or A -> ( B R C \/ B = C \/ C R B ) ) )
16	15	impcom	|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C \/ B = C \/ C R B ) )